Theory "cardinal"

Signature

Definitions

cardeq_def

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

cardleq_def

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

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}

bijns_def

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

Theorems

cardeq_REFL

⊢ ∀s. s ≈ s

cardeq_SYM

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

cardeq_TRANS

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

cardleq_REFL

⊢ ∀s. s ≼ s

cardleq_TRANS

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

cardleq_ANTISYM

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

CARDEQ_FINITE

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

CARDEQ_CARD

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

CARDEQ_0

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

cardeq_INSERT

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

CARDEQ_INSERT_RWT

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

EMPTY_CARDLEQ

⊢ ∅ ≼ t

FINITE_CLE_INFINITE

⊢ FINITE s ∧ INFINITE t ⇒ s ≼ t

CARDEQ_CROSS

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

CARDEQ_CROSS_SYM

⊢ s × t ≈ t × s

CARDEQ_SUBSET_CARDLEQ

⊢ s ≈ t ⇒ s ≼ t

CARDEQ_CARDLEQ

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

CARDLEQ_FINITE

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

INFINITE_UNIV_INF

⊢ INFINITE 𝕌(:α inf)

IMAGE_cardleq

⊢ IMAGE f s ≼ s

CARDLEQ_CROSS_CONG

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

SUBSET_CARDLEQ

⊢ x ⊆ y ⇒ x ≼ y

IMAGE_cardleq_rwt

⊢ s ≼ t ⇒ IMAGE f s ≼ t

countable_thm

⊢ countable s ⇔ s ≼ 𝕌(:num)

countable_cardeq

⊢ s ≈ t ⇒ (countable s ⇔ countable t)

cardleq_dichotomy

⊢ s ≼ t ∨ t ≼ s

cardleq_lteq

⊢ s1 ≼ s2 ⇔ s1 <

cardlt_REFL

⊢ ¬(s <

cardlt_lenoteq

⊢ s <

cardlt_TRANS

⊢ ∀s t u. s <

cardlt_leq_trans

⊢ ∀r s t. r <

cardleq_lt_trans

⊢ ∀r s t. r ≼ s ∧ s <

cardleq_empty

⊢ x ≼ ∅ ⇔ x = ∅


set_binomial2

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


SET_SQUARED_CARDEQ_SET

⊢ INFINITE s ⇒ s × s ≈ s


SET_SUM_CARDEQ_SET

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


CARD_BIGUNION

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


CARD_MUL_ABSORB_LE

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


CARD_MUL_LT_LEMMA

⊢ ∀s t. s ≼ t ∧ t <

CARD_MUL_LT_INFINITE

⊢ ∀s t. s <

BIJ_functions_agree

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


CARD_CARDEQ_I

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


CARDEQ_CARD_EQN

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


CARDLEQ_CARD

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


CARD_LT_CARD

⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 <

EMPTY_set_exp

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


EMPTY_set_exp_CARD

⊢ A ** ∅ ≈ count 1


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}


SING_set_exp_CARD

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


POW_TWO_set_exp

⊢ POW A ≈ count 2 ** A


set_exp_count

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


set_exp_card_cong

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


set_exp_cardle_cong

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


exp_INSERT_cardeq

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


exp_count_cardeq

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


INFINITE_Unum

⊢ INFINITE A ⇔ 𝕌(:num) ≼ A


cardleq_SURJ

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


INFINITE_cardleq_INSERT

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


list_EMPTY

⊢ list ∅ = {[]}


list_SING

⊢ list {e} ≈ 𝕌(:num)


UNIV_list

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


list_BIGUNION_EXP

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


INFINITE_A_list_BIJ_A

⊢ INFINITE A ⇒ list A ≈ A


finite_subsets_bijection

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


FINITE_IMAGE_INJ'

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


countable_decomposition

⊢ ∀s. INFINITE s ⇒ ∃A. BIGUNION A = s ∧ ∀a. a ∈ A ⇒ INFINITE a ∧ countable a


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


count_cardle

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


CANTOR

⊢ A <

cardlt_cardle

⊢ A <

set_exp_product

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


COUNT_EQ_EMPTY

⊢ count n = ∅ ⇔ n = 0


POW_EQ_X_EXP_X

⊢ INFINITE A ⇒ POW A ≈ A ** A


cardeq_bijns_cong

⊢ A ≈ B ⇒ bijns A ≈ bijns B


bijections_cardeq

⊢ INFINITE s ⇒ bijns s ≈ POW s