Theory "cardinal"

Signature

Definitions

set_exp_def

⊢ ∀A B.
      A ** B =
      {f | (∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ (f b = SOME a)) ∧ ∀b. b ∉ B ⇒ (f b = NONE)}

list_def

⊢ ∀A. list A = {l | ∀e. MEM e l ⇒ e ∈ A}

HAS_SIZE

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

cardleq_def

⊢ ∀s1 s2. s1 ≼ s2 ⇔ ∃f. INJ f s1 s2

cardgt_def

⊢ ∀s t. s ≻ t ⇔ t ≺ s

cardgeq_def

⊢ ∀s t. s ≽ t ⇔ t ≼ s

cardeq_def

⊢ ∀s1 s2. s1 ≈ s2 ⇔ ∃f. BIJ f s1 s2

bijns_def

⊢ ∀A. bijns A = {f | THE ∘ f PERMUTES A ∧ ∀a. a ∈ A ⇔ ∃b. f a = SOME b}

add_c

⊢ ∀s t. s + t = {INL x | x ∈ s} ∪ {INR y | y ∈ t}

Theorems

UNIV_list

⊢ 𝕌(:α list) = list 𝕌(:α)

UNION_LE_ADD_C

⊢ ∀s t. s ∪ t ≼ s + t

UNION_ACI

⊢ ∀p q.
      (p ∪ q = q ∪ p) ∧ (p ∪ q ∪ r = p ∪ q ∪ r) ∧ (p ∪ q ∪ r = q ∪ p ∪ r) ∧
      (p ∪ p = p) ∧ (p ∪ p ∪ q = p ∪ q)

SURJECTIVE_RIGHT_INVERSE

⊢ (∀y. ∃x. f x = y) ⇔ ∃g. ∀y. f (g y) = y

SURJECTIVE_ON_RIGHT_INVERSE

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

SURJECTIVE_ON_IMAGE

⊢ ∀f u v.
      (∀t. t ⊆ v ⇒ ∃s. s ⊆ u ∧ (IMAGE f s = t)) ⇔
      ∀y. y ∈ v ⇒ ∃x. x ∈ u ∧ (f x = y)

SURJECTIVE_IMAGE_THM

⊢ ∀f. (∀y. ∃x. f x = y) ⇔ ∀P. IMAGE f {x | P (f x)} = {x | P x}

SURJECTIVE_IMAGE

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

SURJECTIVE_IFF_INJECTIVE_GEN

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

SURJECTIVE_IFF_INJECTIVE

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

SUBSET_CARDLEQ

⊢ ∀x y. x ⊆ y ⇒ x ≼ y

SING_SUBSET

⊢ ∀s x. {x} ⊆ s ⇔ x ∈ s

SING_set_exp_CARD

⊢ {x} ** B ≈ count 1 ∧ A ** {x} ≈ A

SING_set_exp

⊢ ({x} ** B = {(λb. if b ∈ B then SOME x else NONE)}) ∧
  (A ** {x} = {(λb. if b = x then SOME a else NONE) | a ∈ A})

SET_SUM_CARDEQ_SET

⊢ INFINITE s ⇒ s ≈ {T; F} × s ∧ ∀A B. DISJOINT A B ∧ A ≈ s ∧ B ≈ s ⇒ A ∪ B ≈ s

SET_SQUARED_CARDEQ_SET

⊢ ∀s. INFINITE s ⇒ s × s ≈ s

set_exp_product

⊢ (A ** B1) ** B2 ≈ A ** (B1 × B2)

set_exp_count

⊢ A ** count n ≈ {l | (LENGTH l = n) ∧ ∀e. MEM e l ⇒ e ∈ A}

set_exp_cardle_cong

⊢ ((b = ∅) ⇒ (d = ∅)) ⇒ a ≼ b ∧ c ≼ d ⇒ a ** c ≼ b ** d

set_exp_card_cong

⊢ a1 ≈ a2 ⇒ b1 ≈ b2 ⇒ a1 ** b1 ≈ a2 ** b2

set_binomial2

⊢ (A ∪ B) × (A ∪ B) = A × A ∪ A × B ∪ B × A ∪ B × B

RIGHT_IMP_FORALL_THM

⊢ ∀P Q. P ⇒ (∀x. Q x) ⇔ ∀x. P ⇒ Q x

RIGHT_IMP_EXISTS_THM

⊢ ∀P Q. P ⇒ (∃x. Q x) ⇔ ∃x. P ⇒ Q x

POW_TWO_set_exp

⊢ POW A ≈ count 2 ** A

POW_EQ_X_EXP_X

⊢ INFINITE A ⇒ POW A ≈ A ** A

OR_EXISTS_THM

⊢ ∀P Q. (∃x. P x) ∨ (∃x. Q x) ⇔ ∃x. P x ∨ Q x

num_INFINITE

⊢ INFINITE 𝕌(:num)

num_FINITE_AVOID

⊢ ∀s. FINITE s ⇒ ∃a. a ∉ s

num_FINITE

⊢ ∀s. FINITE s ⇔ ∃a. ∀x. x ∈ s ⇒ x ≤ a

NUM_COUNTABLE

⊢ COUNTABLE 𝕌(:num)

mul_c

⊢ ∀s t. s × t = {(x,y) | x ∈ s ∧ y ∈ t}

LT_SUC_LE

⊢ ∀m n. m < SUC n ⇔ m ≤ n

LT_NZ

⊢ ∀n. 0 < n ⇔ n ≠ 0

LT_LE

⊢ ∀m n. m < n ⇔ m ≤ n ∧ m ≠ n

LT_CASES

⊢ ∀m n. m < n ∨ n < m ∨ (m = n)

lt_c

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ s ≺ t

LT

⊢ (∀m. m < 0 ⇔ F) ∧ ∀m n. m < SUC n ⇔ (m = n) ∨ m < n

list_SING

⊢ list {e} ≈ 𝕌(:num)

list_EMPTY

⊢ list ∅ = {[]}

list_BIGUNION_EXP

⊢ list A ≈ BIGUNION (IMAGE (λn. A ** count n) 𝕌(:num))

LEFT_IMP_FORALL_THM

⊢ ∀P Q. (∀x. P x) ⇒ Q ⇔ ∃x. P x ⇒ Q

LEFT_IMP_EXISTS_THM

⊢ ∀P Q. (∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q

LE_SUC_LT

⊢ ∀m n. SUC m ≤ n ⇔ m < n

LE_CASES

⊢ ∀m n. m ≤ n ∨ n ≤ m

LE_C

⊢ ∀s t. s ≼ t ⇔ ∃g. ∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ (g y = x)

le_c

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

LE_1

⊢ (∀n. n ≠ 0 ⇒ 0 < n) ∧ (∀n. n ≠ 0 ⇒ 1 ≤ n) ∧ (∀n. 0 < n ⇒ n ≠ 0) ∧
  (∀n. 0 < n ⇒ 1 ≤ n) ∧ (∀n. 1 ≤ n ⇒ 0 < n) ∧ ∀n. 1 ≤ n ⇒ n ≠ 0

INTER_ACI

⊢ ∀p q.
      (p ∩ q = q ∩ p) ∧ (p ∩ q ∩ r = p ∩ q ∩ r) ∧ (p ∩ q ∩ r = q ∩ p ∩ r) ∧
      (p ∩ p = p) ∧ (p ∩ p ∩ q = p ∩ q)

INJECTIVE_ON_LEFT_INVERSE

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

INJECTIVE_ON_IMAGE

⊢ ∀f u.
      (∀s t. s ⊆ u ∧ t ⊆ u ∧ (IMAGE f s = IMAGE f t) ⇒ (s = t)) ⇔
      ∀x y. x ∈ u ∧ y ∈ u ∧ (f x = f y) ⇒ (x = y)

INJECTIVE_LEFT_INVERSE

⊢ (∀x y. (f x = f y) ⇒ (x = y)) ⇔ ∃g. ∀x. g (f x) = x

INJECTIVE_IMAGE

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

INFINITE_Unum

⊢ INFINITE A ⇔ 𝕌(:num) ≼ A

INFINITE_UNIV_INF

⊢ INFINITE 𝕌(:num + α)

INFINITE_NONEMPTY

⊢ ∀s. INFINITE s ⇒ s ≠ ∅

INFINITE_IMAGE_INJ

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

INFINITE_DIFF_FINITE

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

INFINITE_cardleq_INSERT

⊢ INFINITE A ⇒ (x INSERT s ≼ A ⇔ s ≼ A)

INFINITE_CARD_LE

⊢ ∀s. INFINITE s ⇔ 𝕌(:num) ≼ s

INFINITE_A_list_BIJ_A

⊢ INFINITE A ⇒ list A ≈ A

IN_ELIM_PAIR_THM

⊢ ∀P a b. (a,b) ∈ {(x,y) | P x y} ⇔ P a b

IN_CARD_MUL

⊢ ∀s t x y. (x,y) ∈ s × t ⇔ x ∈ s ∧ y ∈ t

IN_CARD_ADD

⊢ (∀x. INL x ∈ s + t ⇔ x ∈ s) ∧ ∀y. INR y ∈ s + t ⇔ y ∈ t

IMP_CONJ_ALT

⊢ ∀p q. p ∧ q ⇒ r ⇔ q ⇒ p ⇒ r

IMAGE_cardleq_rwt

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

IMAGE_cardleq

⊢ ∀f s. IMAGE f s ≼ s

HAS_SIZE_SUC

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

HAS_SIZE_NUMSEG_LT

⊢ ∀n. {m | m < n} HAS_SIZE n

HAS_SIZE_NUMSEG_LE

⊢ ∀n. {m | m ≤ n} HAS_SIZE n + 1

HAS_SIZE_INDEX

⊢ ∀s n.
      s HAS_SIZE n ⇒
      ∃f. (∀m. m < n ⇒ f m ∈ s) ∧ ∀x. x ∈ s ⇒ ∃!m. m < n ∧ (f m = x)

HAS_SIZE_CLAUSES

⊢ ∀s.
      (s HAS_SIZE 0 ⇔ (s = ∅)) ∧
      (s HAS_SIZE SUC n ⇔ ∃a t. t HAS_SIZE n ∧ a ∉ t ∧ (s = a INSERT t))

HAS_SIZE_CART_UNIV

⊢ ∀m. 𝕌(:α) HAS_SIZE m ⇒ 𝕌(:α) HAS_SIZE m ** 1

HAS_SIZE_CARD

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

HAS_SIZE_BOOL

⊢ 𝕌(:bool) HAS_SIZE 2

HAS_SIZE_0

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

gt_c

⊢ ∀s t. s ≻ t ⇔ t ≺ s

GE_C

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

ge_c

⊢ ∀s t. s ≽ t ⇔ t ≼ s

GE

⊢ ∀n m. m ≥ n ⇔ n ≤ m

FORALL_COUNTABLE_AS_IMAGE

⊢ (∀d. COUNTABLE d ⇒ P d) ⇔ P ∅ ∧ ∀f. P (IMAGE f 𝕌(:num))

finite_subsets_bijection

⊢ INFINITE A ⇒ A ≈ {s | FINITE s ∧ s ⊆ A}

FINITE_PRODUCT_DEPENDENT

⊢ ∀f s t.
      FINITE s ∧ (∀x. x ∈ s ⇒ FINITE (t x)) ⇒ FINITE {f x y | x ∈ s ∧ y ∈ t x}

FINITE_PRODUCT

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE {(x,y) | x ∈ s ∧ y ∈ t}

FINITE_NUMSEG_LT

⊢ ∀n. FINITE {m | m < n}

FINITE_NUMSEG_LE

⊢ ∀n. FINITE {m | m ≤ n}

FINITE_IMP_COUNTABLE

⊢ ∀s. FINITE s ⇒ COUNTABLE s

FINITE_IMAGE_INJ_GENERAL

⊢ ∀f A s.
      (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ∧ FINITE A ⇒
      FINITE {x | x ∈ s ∧ f x ∈ A}

FINITE_IMAGE_INJ_EQ

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

FINITE_IMAGE_INJ'

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

FINITE_IMAGE_INJ

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

FINITE_HAS_SIZE

⊢ ∀s. FINITE s ⇔ s HAS_SIZE CARD s

FINITE_FINITE_BIGUNIONS

⊢ ∀s. FINITE s ⇒ (FINITE (BIGUNION s) ⇔ ∀t. t ∈ s ⇒ FINITE t)

FINITE_FINITE_BIGUNION

⊢ ∀s. FINITE s ⇒ (FINITE (BIGUNION s) ⇔ ∀t. t ∈ s ⇒ FINITE t)

FINITE_CLE_INFINITE

⊢ FINITE s ∧ INFINITE t ⇒ s ≼ t

FINITE_CART_UNIV

⊢ FINITE 𝕌(:α) ⇒ FINITE 𝕌(:α)

FINITE_CARD_LT

⊢ ∀s. FINITE s ⇔ s ≺ 𝕌(:num)

FINITE_BOOL

⊢ FINITE 𝕌(:bool)

exp_INSERT_cardeq

⊢ e ∉ s ⇒ A ** (e INSERT s) ≈ A × A ** s

exp_count_cardeq

⊢ INFINITE A ∧ 0 < n ⇒ A ** count n ≈ A

EQ_C

⊢ ∀s t.
      s ≈ t ⇔
      ∃R.
          (∀x y. R (x,y) ⇒ x ∈ s ∧ y ∈ t) ∧
          (∀x. x ∈ s ⇒ ∃!y. y ∈ t ∧ R (x,y)) ∧
          ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ R (x,y)

eq_c

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

EMPTY_set_exp_CARD

⊢ A ** ∅ ≈ count 1

EMPTY_set_exp

⊢ (A ** ∅ = {K NONE}) ∧ (B ≠ ∅ ⇒ (∅ ** B = ∅))

EMPTY_CARDLEQ

⊢ ∅ ≼ t

disjoint_countable_decomposition

⊢ ∀s.
      INFINITE s ⇒
      ∃A.
          (BIGUNION A = s) ∧ (∀a. a ∈ A ⇒ INFINITE a ∧ COUNTABLE a) ∧
          ∀a1 a2. a1 ∈ A ∧ a2 ∈ A ∧ a1 ≠ a2 ⇒ DISJOINT a1 a2

COUNTABLE_UNION_IMP

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

COUNTABLE_UNION

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

countable_thm

⊢ ∀s. COUNTABLE s ⇔ s ≼ 𝕌(:num)

COUNTABLE_SING

⊢ ∀x. COUNTABLE {x}

COUNTABLE_RESTRICT

⊢ ∀s P. COUNTABLE s ⇒ COUNTABLE {x | x ∈ s ∧ P x}

COUNTABLE_PRODUCT_DEPENDENT

⊢ ∀f s t.
      COUNTABLE s ∧ (∀x. x ∈ s ⇒ COUNTABLE (t x)) ⇒
      COUNTABLE {f x y | x ∈ s ∧ y ∈ t x}

COUNTABLE_INTER

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

COUNTABLE_INSERT

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

COUNTABLE_IMAGE_INJ_GENERAL

⊢ ∀f A s.
      (∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ∧ COUNTABLE A ⇒
      COUNTABLE {x | x ∈ s ∧ f x ∈ A}

COUNTABLE_IMAGE_INJ_EQ

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

COUNTABLE_IMAGE_INJ

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

COUNTABLE_IMAGE

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

COUNTABLE_EMPTY

⊢ COUNTABLE ∅

COUNTABLE_DIFF_FINITE

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

COUNTABLE_DELETE

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

countable_decomposition

⊢ ∀s. INFINITE s ⇒ ∃A. (BIGUNION A = s) ∧ ∀a. a ∈ A ⇒ INFINITE a ∧ COUNTABLE a

COUNTABLE_CROSS

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

COUNTABLE_CASES

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

countable_cardeq

⊢ ∀s t. s ≈ t ⇒ (COUNTABLE s ⇔ COUNTABLE t)

COUNTABLE_BIGUNION

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

COUNTABLE_AS_INJECTIVE_IMAGE

⊢ ∀s.
      COUNTABLE s ∧ INFINITE s ⇒
      ∃f. (s = IMAGE f 𝕌(:num)) ∧ ∀m n. (f m = f n) ⇒ (m = n)

COUNTABLE_AS_IMAGE_SUBSET_EQ

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

COUNTABLE_AS_IMAGE_SUBSET

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

COUNTABLE_AS_IMAGE

⊢ ∀s. COUNTABLE s ∧ s ≠ ∅ ⇒ ∃f. s = IMAGE f 𝕌(:num)

COUNTABLE_ALT_cardleq

⊢ ∀s. COUNTABLE s ⇔ s ≼ 𝕌(:num)

COUNTABLE

⊢ ∀t. COUNTABLE t ⇔ 𝕌(:num) ≽ t

COUNT_EQ_EMPTY

⊢ (count n = ∅) ⇔ (n = 0)

count_cardle

⊢ count n ≼ A ⇔ FINITE A ⇒ n ≤ CARD A

CONJ_EQ_IMP

⊢ ∀p q. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r

CONJ_ACI

⊢ ∀p q.
      (p ∧ q ⇔ q ∧ p) ∧ ((p ∧ q) ∧ r ⇔ p ∧ q ∧ r) ∧ (p ∧ q ∧ r ⇔ q ∧ p ∧ r) ∧
      (p ∧ p ⇔ p) ∧ (p ∧ p ∧ q ⇔ p ∧ q)

cardlt_TRANS

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

cardlt_REFL

⊢ ∀s. ¬(s ≺ s)

cardlt_leq_trans

⊢ ∀r s t. r ≺ s ∧ s ≼ t ⇒ r ≺ t

cardlt_lenoteq

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ ¬(s ≈ t)

cardlt_cardle

⊢ A ≺ B ⇒ A ≼ B

cardleq_TRANS

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

cardleq_SURJ

⊢ A ≼ B ⇔ (∃f. SURJ f B A) ∨ (A = ∅)

cardleq_REFL

⊢ ∀s. s ≼ s

cardleq_lteq

⊢ ∀s1 s2. s1 ≼ s2 ⇔ s1 ≺ s2 ∨ s1 ≈ s2

cardleq_lt_trans

⊢ ∀r s t. r ≼ s ∧ s ≺ t ⇒ r ≺ t

CARDLEQ_FINITE

⊢ ∀s1 s2. FINITE s2 ∧ s1 ≼ s2 ⇒ FINITE s1

cardleq_empty

⊢ ∀x. x ≼ ∅ ⇔ (x = ∅)

cardleq_dichotomy

⊢ ∀s t. s ≼ t ∨ t ≼ s

CARDLEQ_CROSS_CONG

⊢ ∀x1 x2 y1 y2. x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2

CARDLEQ_CARD

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≼ s2 ⇔ CARD s1 ≤ CARD s2)

cardleq_ANTISYM

⊢ ∀s t. s ≼ t ∧ t ≼ s ⇒ s ≈ t

cardeq_TRANS

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

cardeq_SYM

⊢ ∀s t. s ≈ t ⇔ t ≈ s

CARDEQ_SUBSET_CARDLEQ

⊢ s ≈ t ⇒ s ≼ t

cardeq_REFL

⊢ ∀s. s ≈ s

CARDEQ_INSERT_RWT

⊢ ∀s. INFINITE s ⇒ x INSERT s ≈ s

cardeq_INSERT

⊢ x INSERT s ≈ s ⇔ x ∈ s ∨ INFINITE s

CARDEQ_FINITE

⊢ s1 ≈ s2 ⇒ (FINITE s1 ⇔ FINITE s2)

CARDEQ_CROSS_SYM

⊢ s × t ≈ t × s

CARDEQ_CROSS

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2

CARDEQ_CARDLEQ

⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)

CARDEQ_CARD_EQN

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≈ s2 ⇔ (CARD s1 = CARD s2))

CARDEQ_CARD

⊢ s1 ≈ s2 ∧ FINITE s1 ⇒ (CARD s1 = CARD s2)

cardeq_bijns_cong

⊢ A ≈ B ⇒ bijns A ≈ bijns B

CARDEQ_0

⊢ (x ≈ ∅ ⇔ (x = ∅)) ∧ (∅ ≈ x ⇔ (x = ∅))

CARD_SUBSET_EQ

⊢ ∀a b. FINITE b ∧ a ⊆ b ∧ (CARD a = CARD b) ⇒ (a = b)

CARD_SQUARE_NUM

⊢ 𝕌(:num) × 𝕌(:num) ≈ 𝕌(:num)

CARD_SQUARE_INFINITE

⊢ ∀s. INFINITE s ⇒ s × s ≈ s

CARD_RDISTRIB

⊢ ∀s t u. (s + t) × u ≈ s × u + t × u

CARD_NOT_LT

⊢ ∀s t. ¬(s ≺ t) ⇔ t ≼ s

CARD_NOT_LE

⊢ ∀s t. t ≺ s ⇔ t ≺ s

CARD_MUL_SYM

⊢ ∀s t. s × t ≈ t × s

CARD_MUL_LT_LEMMA

⊢ ∀s t u. s ≼ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u

CARD_MUL_LT_INFINITE

⊢ ∀s t u. s ≺ u ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u

CARD_MUL_FINITE

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

CARD_MUL_CONG

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ s × t ≈ s' × t'

CARD_MUL_ASSOC

⊢ ∀s t u. s × (t × u) ≈ s × t × u

CARD_MUL_ABSORB_LE

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s × t ≼ t

CARD_MUL_ABSORB

⊢ ∀s t. INFINITE t ∧ s ≠ ∅ ∧ s ≼ t ⇒ s × t ≈ t

CARD_MUL2_ABSORB_LE

⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s × t ≼ u

CARD_LTE_TRANS

⊢ ∀s t u. s ≺ t ∧ t ≼ u ⇒ s ≺ u

CARD_LTE_TOTAL

⊢ ∀s t. s ≺ t ∨ t ≼ s

CARD_LT_TRANS

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

CARD_LT_TOTAL

⊢ ∀s t. s ≈ t ∨ s ≺ t ∨ t ≺ s

CARD_LT_REFL

⊢ ∀s. ¬(s ≺ s)

CARD_LT_LE

⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ ¬(s ≈ t)

CARD_LT_IMP_LE

⊢ ∀s t. s ≺ t ⇒ s ≼ t

CARD_LT_FINITE_INFINITE

⊢ ∀s t. FINITE s ∧ INFINITE t ⇒ s ≺ t

CARD_LT_CONG

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≺ t ⇔ s' ≺ t')

CARD_LT_CARD

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≺ t ⇔ CARD s < CARD t)

CARD_LT_ADD

⊢ ∀s s' t t'. s ≺ s' ∧ t ≺ t' ⇒ s + t ≺ s' + t'

CARD_LET_TRANS

⊢ ∀s t u. s ≼ t ∧ t ≺ u ⇒ s ≺ u

CARD_LET_TOTAL

⊢ ∀s t. s ≼ t ∨ t ≺ s

CARD_LE_UNIV

⊢ ∀s. s ≼ 𝕌(:α)

CARD_LE_TRANS

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

CARD_LE_TOTAL

⊢ ∀s t. s ≼ t ∨ t ≼ s

CARD_LE_SUBSET

⊢ ∀s t. s ⊆ t ⇒ s ≼ t

CARD_LE_SQUARE

⊢ ∀s. s ≼ s × s

CARD_LE_RELATIONAL

⊢ ∀R s.
      (∀x y y'. x ∈ s ∧ R x y ∧ R x y' ⇒ (y = y')) ⇒
      {y | ∃x. x ∈ s ∧ R x y} ≼ s

CARD_LE_REFL

⊢ ∀s. s ≼ s

CARD_LE_MUL

⊢ ∀s s' t t'. s ≼ s' ∧ t ≼ t' ⇒ s × t ≼ s' × t'

CARD_LE_LT

⊢ ∀s t. s ≼ t ⇔ s ≺ t ∨ s ≈ t

CARD_LE_INJ

⊢ ∀s t.
      FINITE s ∧ FINITE t ∧ CARD s ≤ CARD t ⇒
      ∃f. IMAGE f s ⊆ t ∧ ∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)

CARD_LE_INFINITE

⊢ ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t

CARD_LE_IMAGE_GEN

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

CARD_LE_IMAGE

⊢ ∀f s. IMAGE f s ≼ s

CARD_LE_FINITE

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

CARD_LE_EQ_SUBSET

⊢ ∀s t. s ≼ t ⇔ ∃u. u ⊆ t ∧ s ≈ u

CARD_LE_EMPTY

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

CARD_LE_COUNTABLE

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

CARD_LE_CONG

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≼ t ⇔ s' ≼ t')

CARD_LE_CARD_IMP

⊢ ∀s t. FINITE t ∧ s ≼ t ⇒ CARD s ≤ CARD t

CARD_LE_CARD

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≼ t ⇔ CARD s ≤ CARD t)

CARD_LE_ANTISYM

⊢ ∀s t. s ≼ t ∧ t ≼ s ⇔ s ≈ t

CARD_LE_ADDR

⊢ ∀s t. s ≼ s + t

CARD_LE_ADDL

⊢ ∀s t. t ≼ s + t

CARD_LE_ADD

⊢ ∀s s' t t'. s ≼ s' ∧ t ≼ t' ⇒ s + t ≼ s' + t'

CARD_LDISTRIB

⊢ ∀s t u. s × (t + u) ≈ s × t + s × u

CARD_INFINITE_CONG

⊢ ∀s t. s ≈ t ⇒ (INFINITE s ⇔ INFINITE t)

CARD_IMAGE_LE

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

CARD_IMAGE_INJ

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

CARD_HAS_SIZE_CONG

⊢ ∀s t n. s HAS_SIZE n ∧ s ≈ t ⇒ t HAS_SIZE n

CARD_FINITE_CONG

⊢ ∀s t. s ≈ t ⇒ (FINITE s ⇔ FINITE t)

CARD_EQ_TRANS

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

CARD_EQ_SYM

⊢ ∀s t. s ≈ t ⇔ t ≈ s

CARD_EQ_REFL

⊢ ∀s. s ≈ s

CARD_EQ_IMP_LE

⊢ ∀s t. s ≈ t ⇒ s ≼ t

CARD_EQ_IMAGE

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

CARD_EQ_FINITE

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

CARD_EQ_EMPTY

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

CARD_EQ_COUNTABLE

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

CARD_EQ_CONG

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≈ t ⇔ s' ≈ t')

CARD_EQ_CARD_IMP

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

CARD_EQ_CARD

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

CARD_EQ_BIJECTIONS

⊢ ∀s t.
      FINITE s ∧ FINITE t ∧ (CARD s = CARD t) ⇒
      ∃f g.
          (∀x. x ∈ s ⇒ f x ∈ t ∧ (g (f x) = x)) ∧
          ∀y. y ∈ t ⇒ g y ∈ s ∧ (f (g y) = y)

CARD_EQ_BIJECTION

⊢ ∀s t.
      FINITE s ∧ FINITE t ∧ (CARD s = CARD t) ⇒
      ∃f.
          (∀x. x ∈ s ⇒ f x ∈ t) ∧ (∀y. y ∈ t ⇒ ∃x. x ∈ s ∧ (f x = y)) ∧
          ∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)

CARD_DISJOINT_UNION

⊢ ∀s t. (s ∩ t = ∅) ⇒ s ∪ t ≈ s + t

CARD_COUNTABLE_CONG

⊢ ∀s t. s ≈ t ⇒ (COUNTABLE s ⇔ COUNTABLE t)

CARD_CART_UNIV

⊢ FINITE 𝕌(:α) ⇒ (CARD 𝕌(:α) = CARD 𝕌(:α) ** 1)

CARD_CARDEQ_I

⊢ FINITE s1 ∧ FINITE s2 ∧ (CARD s1 = CARD s2) ⇒ s1 ≈ s2

CARD_BOOL

⊢ CARD 𝕌(:bool) = 2

CARD_BIGUNION_LE

⊢ ∀s t m n.
      s HAS_SIZE m ∧ (∀x. x ∈ s ⇒ FINITE (t x) ∧ CARD (t x) ≤ n) ⇒
      CARD (BIGUNION {t x | x ∈ s}) ≤ m * n

CARD_BIGUNION

⊢ INFINITE k ∧ s1 ≼ k ∧ (∀e. e ∈ s1 ⇒ e ≼ k) ⇒ BIGUNION s1 ≼ k

CARD_ADD_SYM

⊢ ∀s t. s + t ≈ t + s

CARD_ADD_LE_MUL_INFINITE

⊢ ∀s. INFINITE s ⇒ s + s ≼ s × s

CARD_ADD_FINITE_EQ

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

CARD_ADD_FINITE

⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE (s + t)

CARD_ADD_CONG

⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ s + t ≈ s' + t'

CARD_ADD_C

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

CARD_ADD_ASSOC

⊢ ∀s t u. s + (t + u) ≈ s + t + u

CARD_ADD_ABSORB_LE

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s + t ≼ t

CARD_ADD_ABSORB

⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s + t ≈ t

CARD_ADD2_ABSORB_LT

⊢ ∀s t u. INFINITE u ∧ s ≺ u ∧ t ≺ u ⇒ s + t ≺ u

CARD_ADD2_ABSORB_LE

⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s + t ≼ u

CANTOR_THM_UNIV

⊢ 𝕌(:α) ≺ 𝕌(:α -> bool)

CANTOR_THM

⊢ ∀s. s ≺ {t | t ⊆ s}

CANTOR

⊢ A ≺ POW A

BIJECTIVE_INVERSES

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

BIJECTIVE_INJECTIVE_SURJECTIVE

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

bijections_cardeq

⊢ INFINITE s ⇒ bijns s ≈ POW s

BIJ_functions_agree

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