Theory "pred_set"

Signature

Definitions

BIGINTER

⊢ ∀P. BIGINTER P = {x | ∀s. s ∈ P ⇒ x ∈ s}

BIGUNION

⊢ ∀P. BIGUNION P = {x | ∃s. s ∈ P ∧ x ∈ s}

BIJ_DEF

⊢ ∀f s t. BIJ f s t ⇔ INJ f s t ∧ SURJ f s t

CARD_DEF

⊢ (CARD ∅ = 0) ∧
  ∀s. FINITE s ⇒
      ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

CHOICE_DEF

⊢ ∀s. s ≠ ∅ ⇒ CHOICE s ∈ s

COMPL_DEF

⊢ ∀P. COMPL P = 𝕌(:α) DIFF P

CROSS_DEF

⊢ ∀P Q. P × Q = {p | FST p ∈ P ∧ SND p ∈ Q}

DELETE_DEF

⊢ ∀s x. s DELETE x = s DIFF {x}

DFUNSET

⊢ ∀P Q. P ⟶ Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q x)

DIFF_DEF

⊢ ∀s t. s DIFF t = {x | x ∈ s ∧ x ∉ t}

DISJOINT_DEF

⊢ ∀s t. DISJOINT s t ⇔ (s ∩ t = ∅)

EMPTY_DEF

⊢ ∅ = (λx. F)

FINITE_DEF

⊢ ∀s. FINITE s ⇔ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. P (e INSERT s)) ⇒ P s

FUNSET

⊢ ∀P Q. P → Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q)

GSPECIFICATION

⊢ ∀f v. v ∈ GSPEC f ⇔ ∃x. (v,T) = f x

HAS_SIZE

⊢ ∀s n. s HAS_SIZE n ⇔ FINITE s ∧ (CARD s = n)

IMAGE_DEF

⊢ ∀f s. IMAGE f s = {f x | x ∈ s}

INJ_DEF

⊢ ∀f s t.
    INJ f s t ⇔
    (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y) ⇒ (x = y)

INSERT_DEF

⊢ ∀x s. x INSERT s = {y | (y = x) ∨ y ∈ s}

INTER_DEF

⊢ ∀s t. s ∩ t = {x | x ∈ s ∧ x ∈ t}

LINV_LO

⊢ ∀f s y. LINV f s y = THE (LINV_OPT f s y)

LINV_OPT_def

⊢ ∀f s y.
    LINV_OPT f s y =
    if y ∈ IMAGE f s then SOME (@x. x ∈ s ∧ (f x = y)) else NONE

MAX_SET_DEF

⊢ ∀s. FINITE s ⇒
      (s ≠ ∅ ⇒ MAX_SET s ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ MAX_SET s) ∧
      ((s = ∅) ⇒ (MAX_SET s = 0))

MIN_SET_DEF

⊢ MIN_SET = $LEAST

POW_DEF

⊢ ∀set. POW set = {s | s ⊆ set}

PREIMAGE_def

⊢ ∀f s. PREIMAGE f s = {x | f x ∈ s}

PROD_IMAGE_DEF

⊢ ∀f s. ∏ f s = ITSET (λe acc. f e * acc) s 1

PROD_SET_DEF

⊢ PROD_SET = ∏ I

PSUBSET_DEF

⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ s ≠ t

REL_RESTRICT_DEF

⊢ ∀R s x y. REL_RESTRICT R s x y ⇔ x ∈ s ∧ y ∈ s ∧ R x y

REST_DEF

⊢ ∀s. REST s = s DELETE CHOICE s

RINV_LO

⊢ ∀f s y. RINV f s y = THE (LINV_OPT f s y)

SING_DEF

⊢ ∀s. SING s ⇔ ∃x. s = {x}

SUBSET_DEF

⊢ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t

SUM_IMAGE_DEF

⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0

SUM_SET_DEF

⊢ SUM_SET = ∑ I

SURJ_DEF

⊢ ∀f s t.
    SURJ f s t ⇔ (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∈ t ⇒ ∃y. y ∈ s ∧ (f y = x)

UNION_DEF

⊢ ∀s t. s ∪ t = {x | x ∈ s ∨ x ∈ t}

UNIV_DEF

⊢ 𝕌(:α) = (λx. T)

chooser_def

⊢ (∀s. chooser s 0 = CHOICE s) ∧ ∀s n. chooser s (SUC n) = chooser (REST s) n

count_def

⊢ ∀n. count n = {m | m < n}

countable_def

⊢ ∀s. COUNTABLE s ⇔ ∃f. INJ f s 𝕌(:num)

disjUNION_def

⊢ ∀A B. A ⊔ B = {INL a | a ∈ A} ∪ {INR b | b ∈ B}

enumerate_def

⊢ ∀s. enumerate s = @f. BIJ f 𝕌(:num) s

equiv_on_def

⊢ ∀R s.
    R equiv_on s ⇔
    (∀x. x ∈ s ⇒ R x x) ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ (R x y ⇔ R y x)) ∧
    ∀x y z. x ∈ s ∧ y ∈ s ∧ z ∈ s ∧ R x y ∧ R y z ⇒ R x z

is_measure_maximal_def

⊢ ∀m s x. is_measure_maximal m s x ⇔ x ∈ s ∧ ∀y. y ∈ s ⇒ m y ≤ m x

num_to_pair_def

⊢ ∀n. num_to_pair n = (nfst n,nsnd n)

pair_to_num_def

⊢ ∀m n. pair_to_num (m,n) = m ⊗ n

pairwise_def

⊢ ∀P s. pairwise P s ⇔ ∀e1 e2. e1 ∈ s ∧ e2 ∈ s ⇒ P e1 e2

partition_def

⊢ ∀R s. partition R s = {t | ∃x. x ∈ s ∧ (t = {y | y ∈ s ∧ R x y})}

schroeder_close_def

⊢ ∀f s x. schroeder_close f s x ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

Theorems

ABSORPTION

⊢ ∀x s. x ∈ s ⇔ (x INSERT s = s)

ABSORPTION_RWT

⊢ ∀x s. x ∈ s ⇒ (x INSERT s = s)

ABS_DIFF_SUM_IMAGE

⊢ ∀s. FINITE s ⇒ ABS_DIFF (∑ f s) (∑ g s) ≤ ∑ (λx. ABS_DIFF (f x) (g x)) s

BIGINTER_EMPTY

⊢ BIGINTER ∅ = 𝕌(:α)

BIGINTER_INSERT

⊢ ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B

BIGINTER_INTER

⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q

BIGINTER_SING

⊢ ∀P. BIGINTER {P} = P

BIGINTER_SUBSET

⊢ ∀sp s t. t ∈ s ∧ t ⊆ sp ⇒ BIGINTER s ⊆ sp

BIGINTER_UNION

⊢ ∀s1 s2. BIGINTER (s1 ∪ s2) = BIGINTER s1 ∩ BIGINTER s2

BIGINTER_applied

⊢ BIGINTER B x ⇔ ∀P. P ∈ B ⇒ x ∈ P

BIGUNION_CROSS

⊢ ∀f s t. BIGUNION (IMAGE f s) × t = BIGUNION (IMAGE (λn. f n × t) s)

BIGUNION_EMPTY

⊢ BIGUNION ∅ = ∅

BIGUNION_EQ_EMPTY

⊢ ∀P. ((BIGUNION P = ∅) ⇔ (P = ∅) ∨ (P = {∅})) ∧
      ((∅ = BIGUNION P) ⇔ (P = ∅) ∨ (P = {∅}))

BIGUNION_IMAGE_UNIV

⊢ ∀f N.
    (∀n. N ≤ n ⇒ (f n = ∅)) ⇒
    (BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE f (count N)))

BIGUNION_INSERT

⊢ ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P

BIGUNION_PAIR

⊢ ∀s t. BIGUNION {s; t} = s ∪ t

BIGUNION_SING

⊢ ∀x. BIGUNION {x} = x

BIGUNION_SUBSET

⊢ ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X

BIGUNION_UNION

⊢ ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2

BIGUNION_applied

⊢ ∀x sos. BIGUNION sos x ⇔ ∃s. x ∈ s ∧ s ∈ sos

BIGUNION_partition

⊢ R equiv_on s ⇒ (BIGUNION (partition R s) = s)

BIJ_ALT

⊢ ∀f s t. BIJ f s t ⇔ f ∈ (s → t) ∧ ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ (y = f x)

BIJ_COMPOSE

⊢ ∀f g s t u. BIJ f s t ∧ BIJ g t u ⇒ BIJ (g ∘ f) s u

BIJ_DELETE

⊢ ∀s t f. BIJ f s t ⇒ ∀e. e ∈ s ⇒ BIJ f (s DELETE e) (t DELETE f e)

BIJ_EMPTY

⊢ ∀f. (∀s. BIJ f ∅ s ⇔ (s = ∅)) ∧ ∀s. BIJ f s ∅ ⇔ (s = ∅)

BIJ_FINITE

⊢ ∀f s t. BIJ f s t ∧ FINITE s ⇒ FINITE t

BIJ_FINITE_SUBSET

⊢ ∀f s t. BIJ f 𝕌(:num) s ∧ FINITE t ∧ t ⊆ s ⇒ ∃N. ∀n. N ≤ n ⇒ f n ∉ t

BIJ_ID

⊢ ∀s. (λx. x) PERMUTES s

BIJ_IFF_INV

⊢ ∀f s t.
    BIJ f s t ⇔
    (∀x. x ∈ s ⇒ f x ∈ t) ∧
    ∃g. (∀x. x ∈ t ⇒ g x ∈ s) ∧ (∀x. x ∈ s ⇒ (g (f x) = x)) ∧
        ∀x. x ∈ t ⇒ (f (g x) = x)

BIJ_IMAGE

⊢ ∀f s t. BIJ f s t ⇒ (t = IMAGE f s)

BIJ_IMP_11

⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ ∀x y. (f x = f y) ⇔ (x = y)

BIJ_INJ_SURJ

⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. SURJ g s t) ⇒ ∃h. BIJ h s t

BIJ_INSERT

⊢ ∀f e s t.
    BIJ f (e INSERT s) t ⇔
    e ∉ s ∧ f e ∈ t ∧ BIJ f s (t DELETE f e) ∨ e ∈ s ∧ BIJ f s t

BIJ_INSERT_IMP

⊢ ∀f e s t.
    e ∉ s ∧ BIJ f (e INSERT s) t ⇒
    ∃u. (f e INSERT u = t) ∧ f e ∉ u ∧ BIJ f s u

BIJ_INV

⊢ ∀f s t.
    BIJ f s t ⇒
    ∃g. BIJ g t s ∧ (∀x. x ∈ s ⇒ ((g ∘ f) x = x)) ∧
        ∀x. x ∈ t ⇒ ((f ∘ g) x = x)

BIJ_LINV_BIJ

⊢ ∀f s t. BIJ f s t ⇒ BIJ (LINV f s) t s

BIJ_LINV_INV

⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ (f (LINV f s x) = x)

BIJ_NUM_COUNTABLE

⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇒ COUNTABLE s

BIJ_SYM

⊢ ∀s t. (∃f. BIJ f s t) ⇔ ∃g. BIJ g t s

BIJ_SYM_IMP

⊢ ∀s t. (∃f. BIJ f s t) ⇒ ∃g. BIJ g t s

BIJ_TRANS

⊢ ∀s t u. (∃f. BIJ f s t) ∧ (∃g. BIJ g t u) ⇒ ∃h. BIJ h s u

BIJ_support

⊢ ∀f s' s. f PERMUTES s' ∧ s' ⊆ s ∧ (∀x. x ∉ s' ⇒ (f x = x)) ⇒ f PERMUTES s

CARD_BIGUNION_SAME_SIZED_SETS

⊢ ∀n s.
    FINITE s ∧ (∀e. e ∈ s ⇒ FINITE e ∧ (CARD e = n)) ∧
    (∀e1 e2. e1 ∈ s ∧ e2 ∈ s ∧ e1 ≠ e2 ⇒ DISJOINT e1 e2) ⇒
    (CARD (BIGUNION s) = CARD s * n)

CARD_COUNT

⊢ ∀n. CARD (count n) = n

CARD_CROSS

⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ (CARD (P × Q) = CARD P * CARD Q)

CARD_DELETE

⊢ ∀s. FINITE s ⇒ ∀x. CARD (s DELETE x) = if x ∈ s then CARD s − 1 else CARD s

CARD_DIFF

⊢ ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ (CARD (s DIFF t) = CARD s − CARD (s ∩ t))

CARD_DIFF_EQN

⊢ ∀t s. FINITE s ⇒ (CARD (s DIFF t) = CARD s − CARD (s ∩ t))

CARD_EMPTY

⊢ CARD ∅ = 0

CARD_EQ_0

⊢ ∀s. FINITE s ⇒ ((CARD s = 0) ⇔ (s = ∅))

CARD_IMAGE

⊢ ∀s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s

CARD_INJ_IMAGE

⊢ ∀f s. (∀x y. (f x = f y) ⇔ (x = y)) ∧ FINITE s ⇒ (CARD (IMAGE f s) = CARD s)

CARD_INSERT

⊢ ∀s. FINITE s ⇒
      ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)

CARD_INTER_LESS_EQ

⊢ ∀s. FINITE s ⇒ ∀t. CARD (s ∩ t) ≤ CARD s

CARD_LE_MAX_SET

⊢ FINITE s ⇒ CARD s ≤ MAX_SET s + 1

CARD_POW

⊢ ∀s. FINITE s ⇒ (CARD (POW s) = 2 ** CARD s)

CARD_PSUBSET

⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ CARD t < CARD s

CARD_REST

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ (CARD (REST s) = CARD s − 1)

CARD_SING

⊢ ∀x. CARD {x} = 1

CARD_SING_CROSS

⊢ ∀x P. FINITE P ⇒ (CARD ({x} × P) = CARD P)

CARD_SUBSET

⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ CARD t ≤ CARD s

CARD_UNION

⊢ ∀s. FINITE s ⇒
      ∀t. FINITE t ⇒ (CARD (s ∪ t) + CARD (s ∩ t) = CARD s + CARD t)

CARD_UNION_EQN

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (CARD (s ∪ t) = CARD s + CARD t − CARD (s ∩ t))

CARD_UNION_LE

⊢ FINITE s ∧ FINITE t ⇒ CARD (s ∪ t) ≤ CARD s + CARD t

CARD_disjUNION

⊢ FINITE s ∧ FINITE t ⇒ (CARD (s ⊔ t) = CARD s + CARD t)

CHOICE_INSERT_REST

⊢ ∀s. s ≠ ∅ ⇒ (CHOICE s INSERT REST s = s)

CHOICE_INTRO

⊢ (∃x. x ∈ s) ∧ (∀x. x ∈ s ⇒ P x) ⇒ P (CHOICE s)

CHOICE_NOT_IN_REST

⊢ ∀s. CHOICE s ∉ REST s

CHOICE_SING

⊢ ∀x. CHOICE {x} = x

COMMUTING_ITSET_INSERT

⊢ ∀f s.
    (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
    ∀x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)

COMMUTING_ITSET_RECURSES

⊢ ∀f e s b.
    (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
    (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b))

COMPL_CLAUSES

⊢ ∀s. (COMPL s ∩ s = ∅) ∧ (COMPL s ∪ s = 𝕌(:α))

COMPL_COMPL

⊢ ∀s. COMPL (COMPL s) = s

COMPL_EMPTY

⊢ COMPL ∅ = 𝕌(:α)

COMPL_INTER

⊢ (x ∩ COMPL x = ∅) ∧ (COMPL x ∩ x = ∅)

COMPL_SPLITS

⊢ ∀p q. p ∩ q ∪ COMPL p ∩ q = q

COMPL_UNION

⊢ COMPL (s ∪ t) = COMPL s ∩ COMPL t

COMPL_applied

⊢ ∀x s. COMPL s x ⇔ x ∉ s

COMPONENT

⊢ ∀x s. x ∈ x INSERT s

COUNTABLE_ALT

⊢ ∀s. COUNTABLE s ⇔ ∃f. ∀x. x ∈ s ⇒ ∃n. f n = x

COUNTABLE_ALT_BIJ

⊢ ∀s. COUNTABLE s ⇔ FINITE s ∨ BIJ (enumerate s) 𝕌(:num) s

COUNTABLE_COUNT

⊢ ∀n. COUNTABLE (count n)

COUNTABLE_ENUM

⊢ ∀c. COUNTABLE c ⇔ (c = ∅) ∨ ∃f. c = IMAGE f 𝕌(:num)

COUNTABLE_IMAGE_NUM

⊢ ∀f s. COUNTABLE (IMAGE f s)

COUNTABLE_NUM

⊢ ∀s. COUNTABLE s

COUNTABLE_SUBSET

⊢ ∀s t. s ⊆ t ∧ COUNTABLE t ⇒ COUNTABLE s

COUNT_11

⊢ ∀n1 n2. (count n1 = count n2) ⇔ (n1 = n2)

COUNT_DELETE

⊢ ∀n. count n DELETE n = count n

COUNT_MONO

⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n

COUNT_NOT_EMPTY

⊢ ∀n. 0 < n ⇔ count n ≠ ∅

COUNT_SUC

⊢ ∀n. count (SUC n) = n INSERT count n

COUNT_ZERO

⊢ count 0 = ∅

COUNT_applied

⊢ ∀m n. count n m ⇔ m < n

CROSS_BIGUNION

⊢ ∀f s t. s × BIGUNION (IMAGE f t) = BIGUNION (IMAGE (λn. s × f n) t)

CROSS_EMPTY

⊢ ∀P. (P × ∅ = ∅) ∧ (∅ × P = ∅)

CROSS_EMPTY_EQN

⊢ (s × t = ∅) ⇔ (s = ∅) ∨ (t = ∅)

CROSS_EQNS

⊢ ∀s1 s2. (∅ × s2 = ∅) ∧ ((a INSERT s1) × s2 = IMAGE (λy. (a,y)) s2 ∪ s1 × s2)

CROSS_INSERT_LEFT

⊢ ∀P Q x. (x INSERT P) × Q = {x} × Q ∪ P × Q

CROSS_INSERT_RIGHT

⊢ ∀P Q x. P × (x INSERT Q) = P × {x} ∪ P × Q

CROSS_SINGS

⊢ ∀x y. {x} × {y} = {(x,y)}

CROSS_SUBSET

⊢ ∀P Q P0 Q0. P0 × Q0 ⊆ P × Q ⇔ (P0 = ∅) ∨ (Q0 = ∅) ∨ P0 ⊆ P ∧ Q0 ⊆ Q

CROSS_UNIV

⊢ 𝕌(:α # β) = 𝕌(:α) × 𝕌(:β)

CROSS_applied

⊢ ∀P Q x. (P × Q) x ⇔ FST x ∈ P ∧ SND x ∈ Q

DECOMPOSITION

⊢ ∀s x. x ∈ s ⇔ ∃t. (s = x INSERT t) ∧ x ∉ t

DELETE_COMM

⊢ ∀x y s. s DELETE x DELETE y = s DELETE y DELETE x

DELETE_DELETE

⊢ ∀x s. s DELETE x DELETE x = s DELETE x

DELETE_EQ_SING

⊢ ∀s x. x ∈ s ⇒ ((s DELETE x = ∅) ⇔ (s = {x}))

DELETE_INSERT

⊢ ∀x y s.
    (x INSERT s) DELETE y = if x = y then s DELETE y else x INSERT s DELETE y

DELETE_INTER

⊢ ∀s t x. (s DELETE x) ∩ t = s ∩ t DELETE x

DELETE_NON_ELEMENT

⊢ ∀x s. x ∉ s ⇔ (s DELETE x = s)

DELETE_NON_ELEMENT_RWT

⊢ ∀s x. x ∉ s ⇒ (s DELETE x = s)

DELETE_SUBSET

⊢ ∀x s. s DELETE x ⊆ s

DELETE_SUBSET_INSERT

⊢ ∀s e s2. s DELETE e ⊆ s2 ⇔ s ⊆ e INSERT s2

DELETE_applied

⊢ ∀s x y. (s DELETE y) x ⇔ x ∈ s ∧ x ≠ y

DFUNSET_applied

⊢ ∀f P Q. (P ⟶ Q) f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x

DIFF_BIGINTER

⊢ ∀sp s.
    (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒
    (BIGINTER s = sp DIFF BIGUNION (IMAGE (λu. sp DIFF u) s))

DIFF_BIGINTER1

⊢ ∀sp s. sp DIFF BIGINTER s = BIGUNION (IMAGE (λu. sp DIFF u) s)

DIFF_COMM

⊢ ∀x y z. x DIFF y DIFF z = x DIFF z DIFF y

DIFF_DIFF

⊢ ∀s t. s DIFF t DIFF t = s DIFF t

DIFF_DIFF_SUBSET

⊢ ∀s t. t ⊆ s ⇒ (s DIFF (s DIFF t) = t)

DIFF_EMPTY

⊢ ∀s. s DIFF ∅ = s

DIFF_EQ_EMPTY

⊢ ∀s. s DIFF s = ∅

DIFF_INSERT

⊢ ∀s t x. s DIFF (x INSERT t) = s DELETE x DIFF t

DIFF_INTER

⊢ ∀s t g. (s DIFF t) ∩ g = s ∩ g DIFF t

DIFF_INTER2

⊢ ∀s t. s DIFF t ∩ s = s DIFF t

DIFF_INTER_COMPL

⊢ ∀s t. s DIFF t = s ∩ COMPL t

DIFF_INTER_SUBSET

⊢ ∀r s t. r ⊆ s ⇒ (r DIFF s ∩ t = r DIFF t)

DIFF_SAME_UNION

⊢ ∀x y. (x ∪ y DIFF x = y DIFF x) ∧ (x ∪ y DIFF y = x DIFF y)

DIFF_SUBSET

⊢ ∀s t. s DIFF t ⊆ s

DIFF_UNION

⊢ ∀x y z. x DIFF (y ∪ z) = x DIFF y DIFF z

DIFF_UNIV

⊢ ∀s. s DIFF 𝕌(:α) = ∅

DIFF_applied

⊢ ∀s t x. (s DIFF t) x ⇔ x ∈ s ∧ x ∉ t

DISJOINT_ALT

⊢ ∀s t. DISJOINT s t ⇔ ∀x. x ∈ s ⇒ x ∉ t

DISJOINT_BIGINTER

⊢ ∀X Y P.
    Y ∈ P ∧ DISJOINT Y X ⇒ DISJOINT X (BIGINTER P) ∧ DISJOINT (BIGINTER P) X

DISJOINT_BIGUNION

⊢ (∀s t. DISJOINT (BIGUNION s) t ⇔ ∀s'. s' ∈ s ⇒ DISJOINT s' t) ∧
  ∀s t. DISJOINT t (BIGUNION s) ⇔ ∀s'. s' ∈ s ⇒ DISJOINT t s'

DISJOINT_COUNT

⊢ ∀f. (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
      ∀n. DISJOINT (f n) (BIGUNION (IMAGE f (count n)))

DISJOINT_DELETE_SYM

⊢ ∀s t x. DISJOINT (s DELETE x) t ⇔ DISJOINT (t DELETE x) s

DISJOINT_DIFF

⊢ ∀s t. DISJOINT t (s DIFF t) ∧ DISJOINT (s DIFF t) t

DISJOINT_DIFFS

⊢ ∀f g m n.
    (∀n. f n ⊆ f (SUC n)) ∧ (∀n. g n = f (SUC n) DIFF f n) ∧ m ≠ n ⇒
    DISJOINT (g m) (g n)

DISJOINT_EMPTY

⊢ ∀s. DISJOINT ∅ s ∧ DISJOINT s ∅

DISJOINT_EMPTY_REFL

⊢ ∀s. (s = ∅) ⇔ DISJOINT s s

DISJOINT_EMPTY_REFL_RWT

⊢ ∀s. DISJOINT s s ⇔ (s = ∅)

DISJOINT_IMAGE

⊢ (∀x y. (f x = f y) ⇔ (x = y)) ⇒
  (DISJOINT (IMAGE f s1) (IMAGE f s2) ⇔ DISJOINT s1 s2)

DISJOINT_INSERT

⊢ ∀x s t. DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t

DISJOINT_INSERT'

⊢ ∀x s t. DISJOINT t (x INSERT s) ⇔ DISJOINT t s ∧ x ∉ t

DISJOINT_SING_EMPTY

⊢ ∀x. DISJOINT {x} ∅

DISJOINT_SUBSET

⊢ ∀s t u. DISJOINT s t ∧ u ⊆ t ⇒ DISJOINT s u

DISJOINT_SYM

⊢ ∀s t. DISJOINT s t ⇔ DISJOINT t s

DISJOINT_UNION

⊢ ∀s t u. DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u

DISJOINT_UNION_BOTH

⊢ ∀s t u.
    (DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u) ∧
    (DISJOINT u (s ∪ t) ⇔ DISJOINT s u ∧ DISJOINT t u)

ELT_IN_DELETE

⊢ ∀x s. x ∉ s DELETE x

EMPTY_DELETE

⊢ ∀x. ∅ DELETE x = ∅

EMPTY_DIFF

⊢ ∀s. ∅ DIFF s = ∅

EMPTY_FUNSET

⊢ ∀s. ∅ → s = 𝕌(:α -> β)

EMPTY_IN_POW

⊢ ∀s. ∅ ∈ POW s

EMPTY_NOT_IN_partition

⊢ R equiv_on s ⇒ ∅ ∉ partition R s

EMPTY_NOT_UNIV

⊢ ∅ ≠ 𝕌(:α)

EMPTY_SUBSET

⊢ ∀s. ∅ ⊆ s

EMPTY_UNION

⊢ ∀s t. (s ∪ t = ∅) ⇔ (s = ∅) ∧ (t = ∅)

EMPTY_applied

⊢ ∅ x ⇔ F

ENUMERATE

⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇔ BIJ (enumerate s) 𝕌(:num) s

EQUAL_SING

⊢ ∀x y. ({x} = {y}) ⇔ (x = y)

EQ_SUBSET_SUBSET

⊢ ∀s t. (s = t) ⇒ s ⊆ t ∧ t ⊆ s

EQ_UNIV

⊢ (∀x. x ∈ s) ⇔ (s = 𝕌(:α))

EXISTS_IN_IMAGE

⊢ ∀P f s. (∃y. y ∈ IMAGE f s ∧ P y) ⇔ ∃x. x ∈ s ∧ P (f x)

EXISTS_IN_INSERT

⊢ ∀P a s. (∃x. x ∈ a INSERT s ∧ P x) ⇔ P a ∨ ∃x. x ∈ s ∧ P x

EXPLICIT_ENUMERATE_MONO

⊢ ∀n s. FUNPOW REST n s ⊆ s

EXPLICIT_ENUMERATE_NOT_EMPTY

⊢ ∀n s. INFINITE s ⇒ FUNPOW REST n s ≠ ∅

EXTENSION

⊢ ∀s t. (s = t) ⇔ ∀x. x ∈ s ⇔ x ∈ t

FINITELY_INJECTIVE_IMAGE_FINITE

⊢ ∀f. (∀x. FINITE {y | x = f y}) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

FINITE_BIGINTER

⊢ (∃s. s ∈ P ∧ FINITE s) ⇒ FINITE (BIGINTER P)

FINITE_BIGUNION

⊢ ∀P. FINITE P ∧ (∀s. s ∈ P ⇒ FINITE s) ⇒ FINITE (BIGUNION P)

FINITE_BIGUNION_EQ

⊢ ∀P. FINITE (BIGUNION P) ⇔ FINITE P ∧ ∀s. s ∈ P ⇒ FINITE s

FINITE_BIJ

⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ FINITE t ∧ (CARD s = CARD t)

FINITE_BIJ_CARD

⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ (CARD s = CARD t)

FINITE_BIJ_CARD_EQ

⊢ ∀S. FINITE S ⇒ ∀t f. BIJ f S t ∧ FINITE t ⇒ (CARD S = CARD t)

FINITE_BIJ_COUNT

⊢ ∀s. FINITE s ⇒ ∃f b. BIJ f (count b) s

FINITE_BIJ_COUNT_EQ

⊢ ∀s. FINITE s ⇔ ∃c n. BIJ c (count n) s

FINITE_COMPLETE_INDUCTION

⊢ ∀P. (∀x. (∀y. y ⊂ x ⇒ P y) ⇒ FINITE x ⇒ P x) ⇒ ∀x. FINITE x ⇒ P x

FINITE_COUNT

⊢ ∀n. FINITE (count n)

FINITE_CROSS

⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ FINITE (P × Q)

FINITE_CROSS_EQ

⊢ ∀P Q. FINITE (P × Q) ⇔ (P = ∅) ∨ (Q = ∅) ∨ FINITE P ∧ FINITE Q

FINITE_DELETE

⊢ ∀x s. FINITE (s DELETE x) ⇔ FINITE s

FINITE_DIFF

⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s DIFF t)

FINITE_DIFF_down

⊢ ∀P Q. FINITE (P DIFF Q) ∧ FINITE Q ⇒ FINITE P

FINITE_EMPTY

⊢ FINITE ∅

FINITE_HAS_SIZE

⊢ ∀s. FINITE s ⇔ s HAS_SIZE CARD s

FINITE_INDUCT

⊢ ∀P. P ∅ ∧ (∀s. FINITE s ∧ P s ⇒ ∀e. e ∉ s ⇒ P (e INSERT s)) ⇒
      ∀s. FINITE s ⇒ P s

FINITE_INJ

⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ FINITE s

FINITE_INSERT

⊢ ∀x s. FINITE (x INSERT s) ⇔ FINITE s

FINITE_INTER

⊢ ∀s1 s2. FINITE s1 ∨ FINITE s2 ⇒ FINITE (s1 ∩ s2)

FINITE_ISO_NUM

⊢ ∀s. FINITE s ⇒
      ∃f. (∀n m. n < CARD s ∧ m < CARD s ⇒ (f n = f m) ⇒ (n = m)) ∧
          (s = {f n | n < CARD s})

FINITE_POW

⊢ ∀s. FINITE s ⇒ FINITE (POW s)

FINITE_POW_EQN

⊢ FINITE (POW s) ⇔ FINITE s

FINITE_PREIMAGE

⊢ (∀x y. (f x = f y) ⇔ (x = y)) ∧ FINITE s ⇒ FINITE (PREIMAGE f s)

FINITE_PSUBSET_INFINITE

⊢ ∀s. INFINITE s ⇔ ∀t. FINITE t ⇒ t ⊆ s ⇒ t ⊂ s

FINITE_PSUBSET_UNIV

⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ s ⊂ 𝕌(:α)

FINITE_REST

⊢ ∀s. FINITE s ⇒ FINITE (REST s)

FINITE_REST_EQ

⊢ ∀s. FINITE (REST s) ⇔ FINITE s

FINITE_SING

⊢ ∀x. FINITE {x}

FINITE_SURJ

⊢ FINITE s ∧ SURJ f s t ⇒ FINITE t

FINITE_SURJ_BIJ

⊢ FINITE s ∧ SURJ f s t ∧ (CARD t = CARD s) ⇒ BIJ f s t

FINITE_StrongOrder_WF

⊢ ∀R s. FINITE s ∧ StrongOrder (REL_RESTRICT R s) ⇒ WF (REL_RESTRICT R s)

FINITE_UNION

⊢ ∀s t. FINITE (s ∪ t) ⇔ FINITE s ∧ FINITE t

FINITE_WEAK_ENUMERATE

⊢ ∀s. FINITE s ⇔ ∃f b. ∀e. e ∈ s ⇔ ∃n. n < b ∧ (e = f n)

FINITE_WF_noloops

⊢ ∀s. FINITE s ⇒ (WF (REL_RESTRICT R s) ⇔ irreflexive (REL_RESTRICT R s)⁺)

FINITE_is_measure_maximal

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃x. is_measure_maximal m s x

FINITE_partition

⊢ ∀R s. FINITE s ⇒ FINITE (partition R s) ∧ ∀t. t ∈ partition R s ⇒ FINITE t

FORALL_IN_BIGUNION

⊢ ∀P s. (∀x. x ∈ BIGUNION s ⇒ P x) ⇔ ∀t x. t ∈ s ∧ x ∈ t ⇒ P x

FORALL_IN_IMAGE

⊢ ∀P f s. (∀y. y ∈ IMAGE f s ⇒ P y) ⇔ ∀x. x ∈ s ⇒ P (f x)

FORALL_IN_INSERT

⊢ ∀P a s. (∀x. x ∈ a INSERT s ⇒ P x) ⇔ P a ∧ ∀x. x ∈ s ⇒ P x

FORALL_IN_UNION

⊢ ∀P s t. (∀x. x ∈ s ∪ t ⇒ P x) ⇔ (∀x. x ∈ s ⇒ P x) ∧ ∀x. x ∈ t ⇒ P x

FUNSET_DFUNSET

⊢ ∀x y. x → y = x ⟶ K y

FUNSET_EMPTY

⊢ ∀s f. f ∈ (s → ∅) ⇔ (s = ∅)

FUNSET_INTER

⊢ ∀a b c. a → b ∩ c = (a → b) ∩ (a → c)

FUNSET_THM

⊢ ∀s t f x. f ∈ (s → t) ∧ x ∈ s ⇒ f x ∈ t

FUNSET_applied

⊢ ∀f P Q. (P → Q) f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q

GSPECIFICATION_applied

⊢ ∀f v. GSPEC f v ⇔ ∃x. (v,T) = f x

GSPEC_AND

⊢ ∀P Q. {x | P x ∧ Q x} = {x | P x} ∩ {x | Q x}

GSPEC_EQ

⊢ {x | x = y} = {y}

GSPEC_EQ2

⊢ {x | y = x} = {y}

GSPEC_ETA

⊢ {x | P x} = P

GSPEC_F

⊢ {x | F} = ∅

GSPEC_F_COND

⊢ ∀f. (∀x. ¬SND (f x)) ⇒ (GSPEC f = ∅)

GSPEC_ID

⊢ {x | x ∈ y} = y

GSPEC_IMAGE

⊢ GSPEC f = IMAGE (FST ∘ f) (SND ∘ f)

GSPEC_OR

⊢ ∀P Q. {x | P x ∨ Q x} = {x | P x} ∪ {x | Q x}

GSPEC_PAIR_ETA

⊢ {(x,y) | P x y} = Pᴾ

GSPEC_T

⊢ {x | T} = 𝕌(:α)

HAS_SIZE_0

⊢ ∀s. s HAS_SIZE 0 ⇔ (s = ∅)

HAS_SIZE_CARD

⊢ ∀s n. s HAS_SIZE n ⇒ (CARD s = n)

HAS_SIZE_SUC

⊢ ∀s n. s HAS_SIZE SUC n ⇔ s ≠ ∅ ∧ ∀a. a ∈ s ⇒ s DELETE a HAS_SIZE n

IMAGE_11

⊢ (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ((IMAGE f s1 = IMAGE f s2) ⇔ (s1 = s2))

IMAGE_11_INFINITE

⊢ ∀f. (∀x y. (f x = f y) ⇒ (x = y)) ⇒ ∀s. INFINITE s ⇒ INFINITE (IMAGE f s)

IMAGE_BIGUNION

⊢ ∀f M. IMAGE f (BIGUNION M) = BIGUNION (IMAGE (IMAGE f) M)

IMAGE_COMPOSE

⊢ ∀f g s. IMAGE (f ∘ g) s = IMAGE f (IMAGE g s)

IMAGE_CONG

⊢ ∀f s f' s'.
    (s = s') ∧ (∀x. x ∈ s' ⇒ (f x = f' x)) ⇒ (IMAGE f s = IMAGE f' s')

IMAGE_DELETE

⊢ ∀f x s. x ∉ s ⇒ (IMAGE f (s DELETE x) = IMAGE f s)

IMAGE_EMPTY

⊢ ∀f. IMAGE f ∅ = ∅

IMAGE_EQ_EMPTY

⊢ ∀s f. ((IMAGE f s = ∅) ⇔ (s = ∅)) ∧ ((∅ = IMAGE f s) ⇔ (s = ∅))

IMAGE_EQ_SING

⊢ (IMAGE f s = {z}) ⇔ s ≠ ∅ ∧ ∀x. x ∈ s ⇒ (f x = z)

IMAGE_FINITE

⊢ ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)

IMAGE_I

⊢ IMAGE I s = s

IMAGE_ID

⊢ ∀s. IMAGE (λx. x) s = s

IMAGE_II

⊢ IMAGE I = I

IMAGE_IMAGE

⊢ ∀f g s. IMAGE f (IMAGE g s) = IMAGE (f ∘ g) s

IMAGE_IN

⊢ ∀x s. x ∈ s ⇒ ∀f. f x ∈ IMAGE f s

IMAGE_INSERT

⊢ ∀f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s

IMAGE_INTER

⊢ ∀f s t. IMAGE f (s ∩ t) ⊆ IMAGE f s ∩ IMAGE f t

IMAGE_PREIMAGE

⊢ ∀f s. IMAGE f (PREIMAGE f s) ⊆ s

IMAGE_SING

⊢ ∀f x. IMAGE f {x} = {f x}

IMAGE_SUBSET

⊢ ∀s t. s ⊆ t ⇒ ∀f. IMAGE f s ⊆ IMAGE f t

IMAGE_SUBSET_gen

⊢ ∀f s u t. s ⊆ u ∧ IMAGE f u ⊆ t ⇒ IMAGE f s ⊆ t

IMAGE_SURJ

⊢ ∀f s t. SURJ f s t ⇔ (IMAGE f s = t)

IMAGE_UNION

⊢ ∀f s t. IMAGE f (s ∪ t) = IMAGE f s ∪ IMAGE f t

IMAGE_applied

⊢ ∀y s f. IMAGE f s y ⇔ ∃x. (y = f x) ∧ x ∈ s

INFINITE_DIFF_FINITE

⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ s DIFF t ≠ ∅

INFINITE_EXPLICIT_ENUMERATE

⊢ ∀s. INFINITE s ⇒ INJ (λn. CHOICE (FUNPOW REST n s)) 𝕌(:num) s

INFINITE_INHAB

⊢ ∀P. INFINITE P ⇒ ∃x. x ∈ P

INFINITE_INJ

⊢ ∀f s t. INJ f s t ∧ INFINITE s ⇒ INFINITE t

INFINITE_INJ_NOT_SURJ

⊢ ∀s. INFINITE s ⇔ ∃f. INJ f s s ∧ ¬SURJ f s s

INFINITE_NUM_UNIV

⊢ INFINITE 𝕌(:num)

INFINITE_PAIR_UNIV

⊢ FINITE 𝕌(:α # β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)

INFINITE_SUBSET

⊢ ∀s. INFINITE s ⇒ ∀t. s ⊆ t ⇒ INFINITE t

INFINITE_UNIV

⊢ INFINITE 𝕌(:α) ⇔ ∃f. (∀x y. (f x = f y) ⇒ (x = y)) ∧ ∃y. ∀x. f x ≠ y

INJECTIVE_IMAGE_FINITE

⊢ ∀f. (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s

INJ_BIJ_SUBSET

⊢ s0 ⊆ s ∧ INJ f s t ⇒ BIJ f s0 (IMAGE f s0)

INJ_CARD

⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ CARD s ≤ CARD t

INJ_CARD_IMAGE

⊢ ∀s. FINITE s ⇒ INJ f s t ⇒ (CARD (IMAGE f s) = CARD s)

INJ_CARD_IMAGE_EQ

⊢ INJ f s t ⇒ FINITE s ⇒ (CARD (IMAGE f s) = CARD s)

INJ_COMPOSE

⊢ ∀f g s t u. INJ f s t ∧ INJ g t u ⇒ INJ (g ∘ f) s u

INJ_DELETE

⊢ ∀f s t. INJ f s t ⇒ ∀e. e ∈ s ⇒ INJ f (s DELETE e) (t DELETE f e)

INJ_EMPTY

⊢ ∀f. (∀s. INJ f ∅ s) ∧ ∀s. INJ f s ∅ ⇔ (s = ∅)

INJ_EXTEND

⊢ ∀b s t x y.
    INJ b s t ∧ x ∉ s ∧ y ∉ t ⇒ INJ b⦇x ↦ y⦈ (x INSERT s) (y INSERT t)

INJ_ID

⊢ ∀s. INJ (λx. x) s s

INJ_IFF

⊢ INJ f s t ⇔
  (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ ((f x = f y) ⇔ (x = y))

INJ_IMAGE

⊢ ∀f s t. INJ f s t ⇒ INJ f s (IMAGE f s)

INJ_IMAGE_BIJ

⊢ ∀s f. (∃t. INJ f s t) ⇒ BIJ f s (IMAGE f s)

INJ_IMAGE_SUBSET

⊢ ∀f s t. INJ f s t ⇒ IMAGE f s ⊆ t

INJ_INL

⊢ (∀x. x ∈ s ⇒ INL x ∈ t) ⇒ INJ INL s t

INJ_INR

⊢ (∀x. x ∈ s ⇒ INR x ∈ t) ⇒ INJ INR s t

INJ_INSERT

⊢ ∀f x s t.
    INJ f (x INSERT s) t ⇔
    INJ f s t ∧ f x ∈ t ∧ ∀y. y ∈ s ∧ (f x = f y) ⇒ (x = y)

INJ_LINV_OPT

⊢ INJ f s t ⇒ ∀x y. (LINV_OPT f s y = SOME x) ⇔ (y = f x) ∧ x ∈ s ∧ y ∈ t

INJ_LINV_OPT_IMAGE

⊢ INJ (LINV_OPT f s) (IMAGE f s) (IMAGE SOME s)

INJ_SUBSET

⊢ ∀f s t s0 t0. INJ f s t ∧ s0 ⊆ s ∧ t ⊆ t0 ⇒ INJ f s0 t0

INSERT_COMM

⊢ ∀x y s. x INSERT y INSERT s = y INSERT x INSERT s

INSERT_DELETE

⊢ ∀x s. x ∈ s ⇒ (x INSERT s DELETE x = s)

INSERT_DIFF

⊢ ∀s t x. (x INSERT s) DIFF t = if x ∈ t then s DIFF t else x INSERT s DIFF t

INSERT_EQ_SING

⊢ ∀s x y. (x INSERT s = {y}) ⇔ (x = y) ∧ s ⊆ {y}

INSERT_INSERT

⊢ ∀x s. x INSERT x INSERT s = x INSERT s

INSERT_INTER

⊢ ∀x s t. (x INSERT s) ∩ t = if x ∈ t then x INSERT s ∩ t else s ∩ t

INSERT_SING_UNION

⊢ ∀s x. x INSERT s = {x} ∪ s

INSERT_SUBSET

⊢ ∀x s t. x INSERT s ⊆ t ⇔ x ∈ t ∧ s ⊆ t

INSERT_UNION

⊢ ∀x s t. (x INSERT s) ∪ t = if x ∈ t then s ∪ t else x INSERT s ∪ t

INSERT_UNION_EQ

⊢ ∀x s t. (x INSERT s) ∪ t = x INSERT s ∪ t

INSERT_UNIV

⊢ ∀x. x INSERT 𝕌(:α) = 𝕌(:α)

INSERT_applied

⊢ ∀x y s. (y INSERT s) x ⇔ (x = y) ∨ x ∈ s

INTER_ASSOC

⊢ ∀s t u. s ∩ (t ∩ u) = s ∩ t ∩ u

INTER_BIGUNION

⊢ (∀s t. BIGUNION s ∩ t = BIGUNION {x ∩ t | x ∈ s}) ∧
  ∀s t. t ∩ BIGUNION s = BIGUNION {t ∩ x | x ∈ s}

INTER_COMM

⊢ ∀s t. s ∩ t = t ∩ s

INTER_CROSS

⊢ ∀A B C D. A × B ∩ (C × D) = A ∩ C × (B ∩ D)

INTER_EMPTY

⊢ (∀s. ∅ ∩ s = ∅) ∧ ∀s. s ∩ ∅ = ∅

INTER_FINITE

⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s ∩ t)

INTER_IDEMPOT

⊢ ∀s. s ∩ s = s

INTER_OVER_UNION

⊢ ∀s t u. s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

INTER_SUBSET

⊢ (∀s t. s ∩ t ⊆ s) ∧ ∀s t. t ∩ s ⊆ s

INTER_SUBSET_EQN

⊢ ((A ∩ B = A) ⇔ A ⊆ B) ∧ ((A ∩ B = B) ⇔ B ⊆ A)

INTER_UNION

⊢ ((A ∪ B) ∩ A = A) ∧ ((B ∪ A) ∩ A = A) ∧ (A ∩ (A ∪ B) = A) ∧
  (A ∩ (B ∪ A) = A)

INTER_UNION_COMPL

⊢ ∀s t. s ∩ t = COMPL (COMPL s ∪ COMPL t)

INTER_UNIV

⊢ (∀s. 𝕌(:α) ∩ s = s) ∧ ∀s. s ∩ 𝕌(:α) = s

INTER_applied

⊢ ∀s t x. (s ∩ t) x ⇔ x ∈ s ∧ x ∈ t

IN_ABS

⊢ ∀x P. x ∈ (λx. P x) ⇔ P x

IN_APP

⊢ ∀x P. x ∈ P ⇔ P x

IN_BIGINTER

⊢ x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P

IN_BIGINTER_IMAGE

⊢ ∀x f s. x ∈ BIGINTER (IMAGE f s) ⇔ ∀y. y ∈ s ⇒ x ∈ f y

IN_BIGUNION

⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos

IN_BIGUNION_IMAGE

⊢ ∀f s y. y ∈ BIGUNION (IMAGE f s) ⇔ ∃x. x ∈ s ∧ y ∈ f x

IN_COMPL

⊢ ∀x s. x ∈ COMPL s ⇔ x ∉ s

IN_COUNT

⊢ ∀m n. m ∈ count n ⇔ m < n

IN_CROSS

⊢ ∀P Q x. x ∈ P × Q ⇔ FST x ∈ P ∧ SND x ∈ Q

IN_DELETE

⊢ ∀s x y. x ∈ s DELETE y ⇔ x ∈ s ∧ x ≠ y

IN_DELETE_EQ

⊢ ∀s x x'. (x ∈ s ⇔ x' ∈ s) ⇔ (x ∈ s DELETE x' ⇔ x' ∈ s DELETE x)

IN_DFUNSET

⊢ ∀f P Q. f ∈ P ⟶ Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x

IN_DIFF

⊢ ∀s t x. x ∈ s DIFF t ⇔ x ∈ s ∧ x ∉ t

IN_DISJOINT

⊢ ∀s t. DISJOINT s t ⇔ ¬∃x. x ∈ s ∧ x ∈ t

IN_EQ_UNIV_IMP

⊢ ∀s. (s = 𝕌(:α)) ⇒ ∀v. v ∈ s

IN_FUNSET

⊢ ∀f P Q. f ∈ (P → Q) ⇔ ∀x. x ∈ P ⇒ f x ∈ Q

IN_GSPEC

⊢ ∀y x P. P y ∧ (x = f y) ⇒ x ∈ {f x | P x}

IN_GSPEC_IFF

⊢ y ∈ {x | P x} ⇔ P y

IN_IMAGE

⊢ ∀y s f. y ∈ IMAGE f s ⇔ ∃x. (y = f x) ∧ x ∈ s

IN_INFINITE_NOT_FINITE

⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ ∃x. x ∈ s ∧ x ∉ t

IN_INSERT

⊢ ∀x y s. x ∈ y INSERT s ⇔ (x = y) ∨ x ∈ s

IN_INSERT_EXPAND

⊢ ∀x y P. x ∈ y INSERT P ⇔ (x = y) ∨ x ≠ y ∧ x ∈ P

IN_INTER

⊢ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t

IN_POW

⊢ ∀set e. e ∈ POW set ⇔ e ⊆ set

IN_PREIMAGE

⊢ ∀f s x. x ∈ PREIMAGE f s ⇔ f x ∈ s

IN_REST

⊢ ∀x s. x ∈ REST s ⇔ x ∈ s ∧ x ≠ CHOICE s

IN_SING

⊢ ∀x y. x ∈ {y} ⇔ (x = y)

IN_UNION

⊢ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t

IN_UNIV

⊢ ∀x. x ∈ 𝕌(:α)

IN_disjUNION

⊢ (INL a ∈ A ⊔ B ⇔ a ∈ A) ∧ (INR b ∈ A ⊔ B ⇔ b ∈ B)

ITSET_EMPTY

⊢ ∀f b. ITSET f ∅ b = b

ITSET_IND

⊢ ∀P. (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
      ∀v v1. P v v1

ITSET_INSERT

⊢ ∀s. FINITE s ⇒
      ∀f x b.
        ITSET f (x INSERT s) b =
        ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)

ITSET_THM

⊢ ∀s f b.
    FINITE s ⇒
    (ITSET f s b = if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b))

ITSET_def

⊢ ∀s f b.
    ITSET f s b =
    if FINITE s then if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)
    else ARB

ITSET_ind

⊢ ∀P. (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
      ∀v v1. P v v1

K_SUBSET

⊢ ∀x y. K x ⊆ y ⇔ ¬x ∨ 𝕌(:α) ⊆ y

KoenigsLemma

⊢ ∀R. (∀x. FINITE {y | R x y}) ⇒
      ∀x. INFINITE {y | R꙳ x y} ⇒ ∃f. (f 0 = x) ∧ ∀n. R (f n) (f (SUC n))

KoenigsLemma_WF

⊢ ∀R. (∀x. FINITE {y | R x y}) ∧ WF Rᵀ ⇒ ∀x. FINITE {y | R꙳ x y}

LESS_CARD_DIFF

⊢ ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ CARD t < CARD s ⇒ 0 < CARD (s DIFF t)

LINV_DEF

⊢ ∀f s t. INJ f s t ⇒ ∀x. x ∈ s ⇒ (LINV f s (f x) = x)

LINV_OPT_THM

⊢ (LINV_OPT f s y = SOME x) ⇒ x ∈ s ∧ (f x = y)

MAX_SET_ELIM

⊢ ∀P Q.
    FINITE P ∧ ((P = ∅) ⇒ Q 0) ∧ (∀x. (∀y. y ∈ P ⇒ y ≤ x) ∧ x ∈ P ⇒ Q x) ⇒
    Q (MAX_SET P)

MAX_SET_REWRITES

⊢ (MAX_SET ∅ = 0) ∧ (MAX_SET {e} = e)

MAX_SET_THM

⊢ (MAX_SET ∅ = 0) ∧
  ∀e s. FINITE s ⇒ (MAX_SET (e INSERT s) = MAX e (MAX_SET s))

MAX_SET_UNION

⊢ ∀A B. FINITE A ∧ FINITE B ⇒ (MAX_SET (A ∪ B) = MAX (MAX_SET A) (MAX_SET B))

MEMBER_NOT_EMPTY

⊢ ∀s. (∃x. x ∈ s) ⇔ s ≠ ∅

MIN_SET_ELIM

⊢ ∀P Q. P ≠ ∅ ∧ (∀x. (∀y. y ∈ P ⇒ x ≤ y) ∧ x ∈ P ⇒ Q x) ⇒ Q (MIN_SET P)

MIN_SET_LEM

⊢ ∀s. s ≠ ∅ ⇒ MIN_SET s ∈ s ∧ ∀x. x ∈ s ⇒ MIN_SET s ≤ x

MIN_SET_LEQ_MAX_SET

⊢ ∀s. s ≠ ∅ ∧ FINITE s ⇒ MIN_SET s ≤ MAX_SET s

MIN_SET_THM

⊢ (∀e. MIN_SET {e} = e) ∧
  ∀s e1 e2. MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))

MIN_SET_UNION

⊢ ∀A B.
    FINITE A ∧ FINITE B ∧ A ≠ ∅ ∧ B ≠ ∅ ⇒
    (MIN_SET (A ∪ B) = MIN (MIN_SET A) (MIN_SET B))

NOT_EMPTY_INSERT

⊢ ∀x s. ∅ ≠ x INSERT s

NOT_EMPTY_SING

⊢ ∀x. ∅ ≠ {x}

NOT_EQUAL_SETS

⊢ ∀s t. s ≠ t ⇔ ∃x. x ∈ t ⇔ x ∉ s

NOT_INSERT_EMPTY

⊢ ∀x s. x INSERT s ≠ ∅

NOT_IN_EMPTY

⊢ ∀x. x ∉ ∅

NOT_IN_FINITE

⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ ∃x. x ∉ s

NOT_PSUBSET_EMPTY

⊢ ∀s. ¬(s ⊂ ∅)

NOT_SING_EMPTY

⊢ ∀x. {x} ≠ ∅

NOT_UNIV_PSUBSET

⊢ ∀s. ¬(𝕌(:α) ⊂ s)

NUM_SET_WOP

⊢ ∀s. (∃n. n ∈ s) ⇔ ∃n. n ∈ s ∧ ∀m. m ∈ s ⇒ n ≤ m

PAIR_IN_GSPEC_1

⊢ (a,b) ∈ {(y,x) | P y} ⇔ P a ∧ (b = x)

PAIR_IN_GSPEC_2

⊢ (a,b) ∈ {(x,y) | P y} ⇔ P b ∧ (a = x)

PAIR_IN_GSPEC_IFF

⊢ (x,y) ∈ {(x,y) | P x y} ⇔ P x y

PAIR_IN_GSPEC_same

⊢ (a,b) ∈ {(x,x) | P x} ⇔ P a ∧ (a = b)

PHP

⊢ ∀f s t. FINITE t ∧ CARD t < CARD s ⇒ ¬INJ f s t

POW_EMPTY

⊢ ∀s. POW s ≠ ∅

POW_EQNS

⊢ (POW ∅ = {∅}) ∧
  ∀e s. POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps ∪ ps)

POW_INSERT

⊢ ∀e s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) ∪ POW s

POW_applied

⊢ ∀set e. POW set e ⇔ e ⊆ set

PREIMAGE_ALT

⊢ ∀f s. PREIMAGE f s = s ∘ f

PREIMAGE_BIGUNION

⊢ ∀f s. PREIMAGE f (BIGUNION s) = BIGUNION (IMAGE (PREIMAGE f) s)

PREIMAGE_COMP

⊢ ∀f g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g ∘ f) s

PREIMAGE_COMPL

⊢ ∀f s. PREIMAGE f (COMPL s) = COMPL (PREIMAGE f s)

PREIMAGE_COMPL_INTER

⊢ ∀f t sp. PREIMAGE f (COMPL t) ∩ sp = sp DIFF PREIMAGE f t

PREIMAGE_CROSS

⊢ ∀f a b. PREIMAGE f (a × b) = PREIMAGE (FST ∘ f) a ∩ PREIMAGE (SND ∘ f) b

PREIMAGE_DIFF

⊢ ∀f s t. PREIMAGE f (s DIFF t) = PREIMAGE f s DIFF PREIMAGE f t

PREIMAGE_DISJOINT

⊢ ∀f s t. DISJOINT s t ⇒ DISJOINT (PREIMAGE f s) (PREIMAGE f t)

PREIMAGE_EMPTY

⊢ ∀f. PREIMAGE f ∅ = ∅

PREIMAGE_I

⊢ PREIMAGE I = I

PREIMAGE_IMAGE

⊢ ∀f s. s ⊆ PREIMAGE f (IMAGE f s)

PREIMAGE_INTER

⊢ ∀f s t. PREIMAGE f (s ∩ t) = PREIMAGE f s ∩ PREIMAGE f t

PREIMAGE_K

⊢ ∀x s. PREIMAGE (K x) s = if x ∈ s then 𝕌(:β) else ∅

PREIMAGE_SUBSET

⊢ ∀f s t. s ⊆ t ⇒ PREIMAGE f s ⊆ PREIMAGE f t

PREIMAGE_UNION

⊢ ∀f s t. PREIMAGE f (s ∪ t) = PREIMAGE f s ∪ PREIMAGE f t

PREIMAGE_UNIV

⊢ ∀f. PREIMAGE f 𝕌(:β) = 𝕌(:α)

PREIMAGE_applied

⊢ ∀f s x. PREIMAGE f s x ⇔ f x ∈ s

PROD_IMAGE_THM

⊢ ∀f. (∏ f ∅ = 1) ∧
      ∀e s. FINITE s ⇒ (∏ f (e INSERT s) = f e * ∏ f (s DELETE e))

PROD_SET_EMPTY

⊢ PROD_SET ∅ = 1

PROD_SET_IMAGE_REDUCTION

⊢ ∀f s x.
    FINITE (IMAGE f s) ∧ f x ∉ IMAGE f s ⇒
    (PROD_SET (IMAGE f (x INSERT s)) = f x * PROD_SET (IMAGE f s))

PROD_SET_THM

⊢ (PROD_SET ∅ = 1) ∧
  ∀x s. FINITE s ⇒ (PROD_SET (x INSERT s) = x * PROD_SET (s DELETE x))

PSUBSET_EQN

⊢ ∀s1 s2. s1 ⊂ s2 ⇔ s1 ⊆ s2 ∧ ¬(s2 ⊆ s1)

PSUBSET_FINITE

⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ FINITE t

PSUBSET_INSERT_SUBSET

⊢ ∀s t. s ⊂ t ⇔ ∃x. x ∉ s ∧ x INSERT s ⊆ t

PSUBSET_IRREFL

⊢ ∀s. ¬(s ⊂ s)

PSUBSET_MEMBER

⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ ∃y. y ∈ t ∧ y ∉ s

PSUBSET_SING

⊢ ∀s x. x ⊂ {s} ⇔ (x = ∅)

PSUBSET_SUBSET_TRANS

⊢ ∀s t u. s ⊂ t ∧ t ⊆ u ⇒ s ⊂ u

PSUBSET_TRANS

⊢ ∀s t u. s ⊂ t ∧ t ⊂ u ⇒ s ⊂ u

PSUBSET_UNIV

⊢ ∀s. s ⊂ 𝕌(:α) ⇔ ∃x. x ∉ s

RC_PSUBSET

⊢ RC $PSUBSET = $SUBSET

RC_SUBSET_THM

⊢ RC $SUBSET = $SUBSET

REL_RESTRICT_EMPTY

⊢ REL_RESTRICT R ∅ = ∅ᵣ

REL_RESTRICT_SUBSET

⊢ s1 ⊆ s2 ⇒ REL_RESTRICT R s1 ⊆ᵣ REL_RESTRICT R s2

REST_PSUBSET

⊢ ∀s. s ≠ ∅ ⇒ REST s ⊂ s

REST_SING

⊢ ∀x. REST {x} = ∅

REST_SUBSET

⊢ ∀s. REST s ⊆ s

REST_applied

⊢ ∀x s. REST s x ⇔ x ∈ s ∧ x ≠ CHOICE s

RINV_DEF

⊢ ∀f s t. SURJ f s t ⇒ ∀x. x ∈ t ⇒ (f (RINV f s x) = x)

RTC_PSUBSET

⊢ $PSUBSET꙳ = $SUBSET

RTC_SUBSET_THM

⊢ $SUBSET꙳ = $SUBSET

SCHROEDER_BERNSTEIN

⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. INJ g t s) ⇒ ∃h. BIJ h s t

SCHROEDER_BERNSTEIN_AUTO

⊢ ∀s t. t ⊆ s ∧ (∃f. INJ f s t) ⇒ ∃g. BIJ g s t

SCHROEDER_CLOSE

⊢ ∀f s. x ∈ schroeder_close f s ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s

SCHROEDER_CLOSED

⊢ ∀f s. IMAGE f (schroeder_close f s) ⊆ schroeder_close f s

SCHROEDER_CLOSE_SET

⊢ ∀f s t. f ∈ (s → s) ∧ t ⊆ s ⇒ schroeder_close f t ⊆ s

SCHROEDER_CLOSE_SUBSET

⊢ ∀f s. s ⊆ schroeder_close f s

SET_CASES

⊢ ∀s. (s = ∅) ∨ ∃x t. (s = x INSERT t) ∧ x ∉ t

SET_EQ_SUBSET

⊢ ∀s t. (s = t) ⇔ s ⊆ t ∧ t ⊆ s

SET_MINIMUM

⊢ ∀s M. (∃x. x ∈ s) ⇔ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ M x ≤ M y

SING

⊢ ∀x. SING {x}

SING_DELETE

⊢ ∀x. {x} DELETE x = ∅

SING_EMPTY

⊢ SING ∅ ⇔ F

SING_FINITE

⊢ ∀s. SING s ⇒ FINITE s

SING_IFF_CARD1

⊢ ∀s. SING s ⇔ (CARD s = 1) ∧ FINITE s

SING_IFF_EMPTY_REST

⊢ ∀s. SING s ⇔ s ≠ ∅ ∧ (REST s = ∅)

SING_INSERT

⊢ SING (x INSERT s) ⇔ (s = ∅) ∨ (s = {x})

SING_UNION

⊢ SING (s ∪ t) ⇔
  SING s ∧ (t = ∅) ∨ SING t ∧ (s = ∅) ∨ SING s ∧ SING t ∧ (s = t)

SING_applied

⊢ ∀x y. {y} x ⇔ (x = y)

SPECIFICATION

⊢ ∀P x. x ∈ P ⇔ P x

SUBSET_ADD

⊢ ∀f n d. (∀n. f n ⊆ f (SUC n)) ⇒ f n ⊆ f (n + d)

SUBSET_ANTISYM

⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇒ (s = t)

SUBSET_ANTISYM_EQ

⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇔ (s = t)

SUBSET_BIGINTER

⊢ ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y

SUBSET_BIGUNION

⊢ ∀f g. f ⊆ g ⇒ BIGUNION f ⊆ BIGUNION g

SUBSET_BIGUNION_I

⊢ ∀x P. x ∈ P ⇒ x ⊆ BIGUNION P

SUBSET_CROSS

⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ a × c ⊆ b × d

SUBSET_DELETE

⊢ ∀x s t. s ⊆ t DELETE x ⇔ x ∉ s ∧ s ⊆ t

SUBSET_DELETE_BOTH

⊢ ∀s1 s2 x. s1 ⊆ s2 ⇒ s1 DELETE x ⊆ s2 DELETE x

SUBSET_DIFF

⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇔ s1 ⊆ s2 ∧ DISJOINT s1 s3

SUBSET_DIFF_EMPTY

⊢ ∀s t. (s DIFF t = ∅) ⇔ s ⊆ t

SUBSET_DISJOINT

⊢ ∀s t u v. DISJOINT s t ∧ u ⊆ s ∧ v ⊆ t ⇒ DISJOINT u v

SUBSET_EMPTY

⊢ ∀s. s ⊆ ∅ ⇔ (s = ∅)

SUBSET_EQ_CARD

⊢ ∀s. FINITE s ⇒ ∀t. FINITE t ∧ (CARD s = CARD t) ∧ s ⊆ t ⇒ (s = t)

SUBSET_FINITE

⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ FINITE t

SUBSET_FINITE_I

⊢ ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t

SUBSET_IMAGE

⊢ ∀f s t. s ⊆ IMAGE f t ⇔ ∃u. u ⊆ t ∧ (s = IMAGE f u)

SUBSET_INSERT

⊢ ∀x s. x ∉ s ⇒ ∀t. s ⊆ x INSERT t ⇔ s ⊆ t

SUBSET_INSERT_DELETE

⊢ ∀x s t. s ⊆ x INSERT t ⇔ s DELETE x ⊆ t

SUBSET_INSERT_RIGHT

⊢ ∀e s1 s2. s1 ⊆ s2 ⇒ s1 ⊆ e INSERT s2

SUBSET_INTER

⊢ ∀s t u. s ⊆ t ∩ u ⇔ s ⊆ t ∧ s ⊆ u

SUBSET_INTER1

⊢ ∀s t. s ⊆ t ⇒ (s ∩ t = s)

SUBSET_INTER2

⊢ ∀s t. s ⊆ t ⇒ (t ∩ s = s)

SUBSET_INTER_ABSORPTION

⊢ ∀s t. s ⊆ t ⇔ (s ∩ t = s)

SUBSET_K

⊢ ∀x y. x ⊆ K y ⇔ x ⊆ ∅ ∨ y

SUBSET_MAX_SET

⊢ ∀I J. FINITE I ∧ FINITE J ∧ I ⊆ J ⇒ MAX_SET I ≤ MAX_SET J

SUBSET_MIN_SET

⊢ ∀I J n. I ≠ ∅ ∧ J ≠ ∅ ∧ I ⊆ J ⇒ MIN_SET J ≤ MIN_SET I

SUBSET_OF_INSERT

⊢ ∀x s. s ⊆ x INSERT s

SUBSET_POW

⊢ ∀s1 s2. s1 ⊆ s2 ⇒ POW s1 ⊆ POW s2

SUBSET_PSUBSET_TRANS

⊢ ∀s t u. s ⊆ t ∧ t ⊂ u ⇒ s ⊂ u

SUBSET_REFL

⊢ ∀s. s ⊆ s

SUBSET_THM

⊢ ∀P Q. P ⊆ Q ⇒ ∀x. x ∈ P ⇒ x ∈ Q

SUBSET_TRANS

⊢ ∀s t u. s ⊆ t ∧ t ⊆ u ⇒ s ⊆ u

SUBSET_UNION

⊢ (∀s t. s ⊆ s ∪ t) ∧ ∀s t. s ⊆ t ∪ s

SUBSET_UNION_ABSORPTION

⊢ ∀s t. s ⊆ t ⇔ (s ∪ t = t)

SUBSET_UNIV

⊢ ∀s. s ⊆ 𝕌(:α)

SUBSET_applied

⊢ ∀s t. s ⊆ t ⇔ ∀x. s x ⇒ t x

SUBSET_count_MAX_SET

⊢ FINITE s ⇒ s ⊆ count (MAX_SET s + 1)

SUBSET_reflexive

⊢ reflexive $SUBSET

SUBSET_transitive

⊢ transitive $SUBSET

SUM_IMAGE_CONG

⊢ (s1 = s2) ∧ (∀x. x ∈ s2 ⇒ (f1 x = f2 x)) ⇒ (∑ f1 s1 = ∑ f2 s2)

SUM_IMAGE_DELETE

⊢ ∀f s. FINITE s ⇒ ∀e. ∑ f (s DELETE e) = if e ∈ s then ∑ f s − f e else ∑ f s

SUM_IMAGE_INJ_o

⊢ ∀s. FINITE s ⇒ ∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) s

SUM_IMAGE_IN_LE

⊢ ∀f s e. FINITE s ∧ e ∈ s ⇒ f e ≤ ∑ f s

SUM_IMAGE_MONO_LESS

⊢ ∀s. FINITE s ⇒
      (∃x. x ∈ s ∧ f x < g x) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
      ∑ f s < ∑ g s

SUM_IMAGE_MONO_LESS_EQ

⊢ ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g s

SUM_IMAGE_PERMUTES

⊢ ∀s. FINITE s ⇒ ∀g. g PERMUTES s ⇒ ∀f. ∑ (f ∘ g) s = ∑ f s

SUM_IMAGE_SING

⊢ ∀f e. ∑ f {e} = f e

SUM_IMAGE_SUBSET_LE

⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ ∑ f t ≤ ∑ f s

SUM_IMAGE_THM

⊢ ∀f. (∑ f ∅ = 0) ∧
      ∀e s. FINITE s ⇒ (∑ f (e INSERT s) = f e + ∑ f (s DELETE e))

SUM_IMAGE_UNION

⊢ ∀f s t. FINITE s ∧ FINITE t ⇒ (∑ f (s ∪ t) = ∑ f s + ∑ f t − ∑ f (s ∩ t))

SUM_IMAGE_ZERO

⊢ ∀s. FINITE s ⇒ ((∑ f s = 0) ⇔ ∀x. x ∈ s ⇒ (f x = 0))

SUM_IMAGE_lower_bound

⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ n ≤ f x) ⇒ CARD s * n ≤ ∑ f s

SUM_IMAGE_upper_bound

⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ f x ≤ n) ⇒ ∑ f s ≤ CARD s * n

SUM_SAME_IMAGE

⊢ ∀P. FINITE P ⇒
      ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ (f p = f q)) ⇒ (∑ f P = CARD P * f p)

SUM_SET_DELETE

⊢ ∀s. FINITE s ⇒
      ∀e. SUM_SET (s DELETE e) = if e ∈ s then SUM_SET s − e else SUM_SET s

SUM_SET_EMPTY

⊢ SUM_SET ∅ = 0

SUM_SET_IN_LE

⊢ ∀x s. FINITE s ∧ x ∈ s ⇒ x ≤ SUM_SET s

SUM_SET_SING

⊢ ∀n. SUM_SET {n} = n

SUM_SET_SUBSET_LE

⊢ ∀s t. FINITE t ∧ s ⊆ t ⇒ SUM_SET s ≤ SUM_SET t

SUM_SET_THM

⊢ (SUM_SET ∅ = 0) ∧
  ∀x s. FINITE s ⇒ (SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x))

SUM_SET_UNION

⊢ ∀s t.
    FINITE s ∧ FINITE t ⇒
    (SUM_SET (s ∪ t) = SUM_SET s + SUM_SET t − SUM_SET (s ∩ t))

SUM_SET_count

⊢ SUM_SET (count n) = n * (n − 1) DIV 2

SUM_SET_count_2

⊢ ∀n. 2 * SUM_SET (count n) = n * (n − 1)

SUM_UNIV

⊢ 𝕌(:α + β) = IMAGE INL 𝕌(:α) ∪ IMAGE INR 𝕌(:β)

SURJ_CARD

⊢ ∀s. FINITE s ⇒ ∀t. SURJ f s t ⇒ FINITE t ∧ CARD t ≤ CARD s

SURJ_COMPOSE

⊢ ∀f g s t u. SURJ f s t ∧ SURJ g t u ⇒ SURJ (g ∘ f) s u

SURJ_EMPTY

⊢ ∀f. (∀s. SURJ f ∅ s ⇔ (s = ∅)) ∧ ∀s. SURJ f s ∅ ⇔ (s = ∅)

SURJ_ID

⊢ ∀s. SURJ (λx. x) s s

SURJ_IMAGE

⊢ SURJ f s (IMAGE f s)

SURJ_IMP_INJ

⊢ ∀s t. (∃f. SURJ f s t) ⇒ ∃g. INJ g t s

SURJ_INJ_INV

⊢ SURJ f s t ⇒ ∃g. INJ g t s ∧ ∀y. y ∈ t ⇒ (f (g y) = y)

TC_PSUBSET

⊢ $PSUBSET⁺ = $PSUBSET

TC_SUBSET_THM

⊢ $SUBSET⁺ = $SUBSET

UNION_ASSOC

⊢ ∀s t u. s ∪ (t ∪ u) = s ∪ t ∪ u

UNION_COMM

⊢ ∀s t. s ∪ t = t ∪ s

UNION_DELETE

⊢ ∀A B x. A ∪ B DELETE x = A DELETE x ∪ (B DELETE x)

UNION_DIFF

⊢ s ⊆ t ⇒ (s ∪ (t DIFF s) = t) ∧ (t DIFF s ∪ s = t)

UNION_DIFF_2

⊢ ∀s t. s ∪ (s DIFF t) = s

UNION_DIFF_EQ

⊢ (∀s t. s ∪ (t DIFF s) = s ∪ t) ∧ ∀s t. t DIFF s ∪ s = t ∪ s

UNION_EMPTY

⊢ (∀s. ∅ ∪ s = s) ∧ ∀s. s ∪ ∅ = s

UNION_IDEMPOT

⊢ ∀s. s ∪ s = s

UNION_OVER_INTER

⊢ ∀s t u. s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

UNION_SUBSET

⊢ ∀s t u. s ∪ t ⊆ u ⇔ s ⊆ u ∧ t ⊆ u

UNION_UNIV

⊢ (∀s. 𝕌(:α) ∪ s = 𝕌(:α)) ∧ ∀s. s ∪ 𝕌(:α) = 𝕌(:α)

UNION_applied

⊢ ∀s t x. (s ∪ t) x ⇔ x ∈ s ∨ x ∈ t

UNIQUE_MEMBER_SING

⊢ ∀x s. x ∈ s ∧ (∀y. y ∈ s ⇒ (x = y)) ⇔ (s = {x})

UNIV_BOOL

⊢ 𝕌(:bool) = {T; F}

UNIV_FUNSET_UNIV

⊢ 𝕌(:α) → 𝕌(:β) = 𝕌(:α -> β)

UNIV_FUN_TO_BOOL

⊢ 𝕌(:α -> bool) = POW 𝕌(:α)

UNIV_NOT_EMPTY

⊢ 𝕌(:α) ≠ ∅

UNIV_SUBSET

⊢ ∀s. 𝕌(:α) ⊆ s ⇔ (s = 𝕌(:α))

UNIV_applied

⊢ ∀x. 𝕌(:α) x

X_LE_MAX_SET

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s

bigunion_countable

⊢ ∀s. COUNTABLE s ∧ (∀x. x ∈ s ⇒ COUNTABLE x) ⇒ COUNTABLE (BIGUNION s)

chooser_compute

⊢ (∀s. chooser s 0 = CHOICE s) ∧
  (∀s n.
     chooser s (NUMERAL (BIT1 n)) = chooser (REST s) (NUMERAL (BIT1 n) − 1)) ∧
  ∀s n. chooser s (NUMERAL (BIT2 n)) = chooser (REST s) (NUMERAL (BIT1 n))

compl_insert

⊢ ∀s x. COMPL (x INSERT s) = COMPL s DELETE x

count_EQN

⊢ ∀n. count n = if n = 0 then ∅ else (let p = PRE n in p INSERT count p)

count_add

⊢ ∀n m. count (n + m) = count n ∪ IMAGE ($+ n) (count m)

count_add1

⊢ ∀n. count (n + 1) = n INSERT count n

countable_EMPTY

⊢ COUNTABLE ∅

countable_INSERT

⊢ COUNTABLE (x INSERT s) ⇔ COUNTABLE s

countable_Uprod

⊢ COUNTABLE 𝕌(:α # β) ⇔ COUNTABLE 𝕌(:α) ∧ COUNTABLE 𝕌(:β)

countable_Usum

⊢ COUNTABLE 𝕌(:α + β) ⇔ COUNTABLE 𝕌(:α) ∧ COUNTABLE 𝕌(:β)

countable_image_nats

⊢ COUNTABLE (IMAGE f 𝕌(:num))

countable_surj

⊢ ∀s. COUNTABLE s ⇔ (s = ∅) ∨ ∃f. SURJ f 𝕌(:num) s

cross_countable

⊢ ∀s t. COUNTABLE s ∧ COUNTABLE t ⇒ COUNTABLE (s × t)

cross_countable_IFF

⊢ COUNTABLE (s × t) ⇔ (s = ∅) ∨ (t = ∅) ∨ COUNTABLE s ∧ COUNTABLE t

disjUNION_UNIV

⊢ 𝕌(:α + β) = 𝕌(:α) ⊔ 𝕌(:β)

finite_countable

⊢ ∀s. FINITE s ⇒ COUNTABLE s

image_countable

⊢ ∀f s. COUNTABLE s ⇒ COUNTABLE (IMAGE f s)

in_max_set

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s

infinite_num_inj

⊢ ∀s. INFINITE s ⇔ ∃f. INJ f 𝕌(:num) s

infinite_pow_uncountable

⊢ ∀s. INFINITE s ⇒ ¬COUNTABLE (POW s)

infinite_rest

⊢ ∀s. INFINITE s ⇒ INFINITE (REST s)

inj_countable

⊢ ∀f s t. COUNTABLE t ∧ INJ f s t ⇒ COUNTABLE s

inj_image_countable_IFF

⊢ INJ f s (IMAGE f s) ⇒ (COUNTABLE (IMAGE f s) ⇔ COUNTABLE s)

inj_surj

⊢ ∀f s t. INJ f s t ⇒ (s = ∅) ∨ ∃f'. SURJ f' t s

inter_countable

⊢ ∀s t. COUNTABLE s ∨ COUNTABLE t ⇒ COUNTABLE (s ∩ t)

is_measure_maximal_INSERT

⊢ ∀x s m e y.
    x ∈ s ∧ m e < m x ⇒
    (is_measure_maximal m (e INSERT s) y ⇔ is_measure_maximal m s y)

is_measure_maximal_SING

⊢ is_measure_maximal m {x} y ⇔ (y = x)

num_countable

⊢ COUNTABLE 𝕌(:num)

pair_to_num_formula

⊢ ∀x y. pair_to_num (x,y) = (x + y + 1) * (x + y) DIV 2 + y

pair_to_num_inv

⊢ (∀x. pair_to_num (num_to_pair x) = x) ∧
  ∀x y. num_to_pair (pair_to_num (x,y)) = (x,y)

pairwise_SUBSET

⊢ ∀R s t. pairwise R t ∧ s ⊆ t ⇒ pairwise R s

pairwise_UNION

⊢ pairwise R (s1 ∪ s2) ⇔
  pairwise R s1 ∧ pairwise R s2 ∧ ∀x y. x ∈ s1 ∧ y ∈ s2 ⇒ R x y ∧ R y x

partition_CARD

⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ (CARD s = ∑ CARD (partition R s))

partition_SUBSET

⊢ ∀R s t. t ∈ partition R s ⇒ t ⊆ s

partition_elements_disjoint

⊢ R equiv_on s ⇒
  ∀t1 t2. t1 ∈ partition R s ∧ t2 ∈ partition R s ∧ t1 ≠ t2 ⇒ DISJOINT t1 t2

partition_elements_interrelate

⊢ R equiv_on s ⇒ ∀t. t ∈ partition R s ⇒ ∀x y. x ∈ t ∧ y ∈ t ⇒ R x y

pow_no_surj

⊢ ∀s. ¬∃f. SURJ f s (POW s)

subset_countable

⊢ ∀s t. COUNTABLE s ∧ t ⊆ s ⇒ COUNTABLE t

transitive_PSUBSET

⊢ transitive $PSUBSET

union_countable

⊢ ∀s t. COUNTABLE s ∧ COUNTABLE t ⇒ COUNTABLE (s ∪ t)

union_countable_IFF

⊢ COUNTABLE (s ∪ t) ⇔ COUNTABLE s ∧ COUNTABLE t