Structure cardinalTheory
signature cardinalTheory =
sig
type thm = Thm.thm
(* Definitions *)
val add_c : thm
val bijns_def : thm
val cardeq_def : thm
val cardgeq_def : thm
val cardgt_def : thm
val cardleq_def : thm
val list_def : thm
val set_exp_def : thm
(* Theorems *)
val BIJECTIVE_INJECTIVE_SURJECTIVE : thm
val BIJECTIVE_INVERSES : thm
val BIJ_functions_agree : thm
val CANTOR : thm
val CANTOR_THM : thm
val CANTOR_THM_UNIV : thm
val CARDEQ_0 : thm
val CARDEQ_CARD : thm
val CARDEQ_CARDLEQ : thm
val CARDEQ_CARD_EQN : thm
val CARDEQ_CROSS : thm
val CARDEQ_CROSS_SYM : thm
val CARDEQ_FINITE : thm
val CARDEQ_INSERT_RWT : thm
val CARDEQ_SUBSET_CARDLEQ : thm
val CARDLEQ_CARD : thm
val CARDLEQ_CROSS_CONG : thm
val CARDLEQ_FINITE : thm
val CARD_ADD2_ABSORB_LE : thm
val CARD_ADD2_ABSORB_LT : thm
val CARD_ADD_ABSORB : thm
val CARD_ADD_ABSORB_LE : thm
val CARD_ADD_ASSOC : thm
val CARD_ADD_C : thm
val CARD_ADD_CONG : thm
val CARD_ADD_FINITE : thm
val CARD_ADD_FINITE_EQ : thm
val CARD_ADD_LE_MUL_INFINITE : thm
val CARD_ADD_SYM : thm
val CARD_BIGUNION : thm
val CARD_BIGUNION_LE : thm
val CARD_BOOL : thm
val CARD_CARDEQ_I : thm
val CARD_CART_UNIV : thm
val CARD_COUNTABLE_CONG : thm
val CARD_DISJOINT_UNION : thm
val CARD_EQ_BIJECTION : thm
val CARD_EQ_BIJECTIONS : thm
val CARD_EQ_CARD : thm
val CARD_EQ_CARD_IMP : thm
val CARD_EQ_CONG : thm
val CARD_EQ_COUNTABLE : thm
val CARD_EQ_EMPTY : thm
val CARD_EQ_FINITE : thm
val CARD_EQ_IMAGE : thm
val CARD_EQ_IMP_LE : thm
val CARD_EQ_REFL : thm
val CARD_EQ_SYM : thm
val CARD_EQ_TRANS : thm
val CARD_FINITE_CONG : thm
val CARD_HAS_SIZE_CONG : thm
val CARD_IMAGE_INJ : thm
val CARD_IMAGE_LE : thm
val CARD_INFINITE_CONG : thm
val CARD_LDISTRIB : thm
val CARD_LET_TOTAL : thm
val CARD_LET_TRANS : thm
val CARD_LE_ADD : thm
val CARD_LE_ADDL : thm
val CARD_LE_ADDR : thm
val CARD_LE_ANTISYM : thm
val CARD_LE_CARD : thm
val CARD_LE_CARD_IMP : thm
val CARD_LE_CONG : thm
val CARD_LE_COUNTABLE : thm
val CARD_LE_EMPTY : thm
val CARD_LE_EQ_SUBSET : thm
val CARD_LE_FINITE : thm
val CARD_LE_IMAGE : thm
val CARD_LE_IMAGE_GEN : thm
val CARD_LE_INFINITE : thm
val CARD_LE_INJ : thm
val CARD_LE_LT : thm
val CARD_LE_MUL : thm
val CARD_LE_REFL : thm
val CARD_LE_RELATIONAL : thm
val CARD_LE_SQUARE : thm
val CARD_LE_SUBSET : thm
val CARD_LE_TOTAL : thm
val CARD_LE_TRANS : thm
val CARD_LE_UNIV : thm
val CARD_LTE_TOTAL : thm
val CARD_LTE_TRANS : thm
val CARD_LT_ADD : thm
val CARD_LT_CARD : thm
val CARD_LT_CONG : thm
val CARD_LT_FINITE_INFINITE : thm
val CARD_LT_IMP_LE : thm
val CARD_LT_LE : thm
val CARD_LT_REFL : thm
val CARD_LT_TOTAL : thm
val CARD_LT_TRANS : thm
val CARD_MUL2_ABSORB_LE : thm
val CARD_MUL_ABSORB : thm
val CARD_MUL_ABSORB_LE : thm
val CARD_MUL_ASSOC : thm
val CARD_MUL_CONG : thm
val CARD_MUL_FINITE : thm
val CARD_MUL_LT_INFINITE : thm
val CARD_MUL_LT_LEMMA : thm
val CARD_MUL_SYM : thm
val CARD_NOT_LE : thm
val CARD_NOT_LT : thm
val CARD_RDISTRIB : thm
val CARD_SQUARE_INFINITE : thm
val CARD_SQUARE_NUM : thm
val CARD_SUBSET_EQ : thm
val CONJ_ACI : thm
val CONJ_EQ_IMP : thm
val COUNTABLE : thm
val COUNTABLE_ALT_cardleq : thm
val COUNTABLE_AS_IMAGE : thm
val COUNTABLE_AS_IMAGE_SUBSET : thm
val COUNTABLE_AS_IMAGE_SUBSET_EQ : thm
val COUNTABLE_AS_INJECTIVE_IMAGE : thm
val COUNTABLE_BIGUNION : thm
val COUNTABLE_CASES : thm
val COUNTABLE_CROSS : thm
val COUNTABLE_DELETE : thm
val COUNTABLE_DIFF_FINITE : thm
val COUNTABLE_EMPTY : thm
val COUNTABLE_IMAGE : thm
val COUNTABLE_IMAGE_INJ : thm
val COUNTABLE_IMAGE_INJ_EQ : thm
val COUNTABLE_IMAGE_INJ_GENERAL : thm
val COUNTABLE_INSERT : thm
val COUNTABLE_INTER : thm
val COUNTABLE_PRODUCT_DEPENDENT : thm
val COUNTABLE_RESTRICT : thm
val COUNTABLE_SING : thm
val COUNTABLE_UNION : thm
val COUNTABLE_UNION_IMP : thm
val COUNT_EQ_EMPTY : thm
val EMPTY_CARDLEQ : thm
val EMPTY_set_exp : thm
val EMPTY_set_exp_CARD : thm
val EQ_C : thm
val FINITE_BOOL : thm
val FINITE_CARD_LT : thm
val FINITE_CART_UNIV : thm
val FINITE_CLE_INFINITE : thm
val FINITE_FINITE_BIGUNION : thm
val FINITE_FINITE_BIGUNIONS : thm
val FINITE_IMAGE_INJ : thm
val FINITE_IMAGE_INJ' : thm
val FINITE_IMAGE_INJ_EQ : thm
val FINITE_IMAGE_INJ_GENERAL : thm
val FINITE_IMP_COUNTABLE : thm
val FINITE_NUMSEG_LE : thm
val FINITE_NUMSEG_LT : thm
val FINITE_PRODUCT : thm
val FINITE_PRODUCT_DEPENDENT : thm
val FORALL_COUNTABLE_AS_IMAGE : thm
val GE : thm
val GE_C : thm
val HAS_SIZE_BOOL : thm
val HAS_SIZE_CART_UNIV : thm
val HAS_SIZE_CLAUSES : thm
val HAS_SIZE_INDEX : thm
val HAS_SIZE_NUMSEG_LE : thm
val HAS_SIZE_NUMSEG_LT : thm
val IMAGE_cardleq : thm
val IMAGE_cardleq_rwt : thm
val IMP_CONJ_ALT : thm
val INFINITE_A_list_BIJ_A : thm
val INFINITE_CARD_LE : thm
val INFINITE_DIFF_FINITE : thm
val INFINITE_IMAGE_INJ : thm
val INFINITE_NONEMPTY : thm
val INFINITE_UNIV_INF : thm
val INFINITE_Unum : thm
val INFINITE_cardleq_INSERT : thm
val INJECTIVE_IMAGE : thm
val INJECTIVE_LEFT_INVERSE : thm
val INJECTIVE_ON_IMAGE : thm
val INJECTIVE_ON_LEFT_INVERSE : thm
val INTER_ACI : thm
val IN_CARD_ADD : thm
val IN_CARD_MUL : thm
val IN_ELIM_PAIR_THM : thm
val LEFT_IMP_EXISTS_THM : thm
val LEFT_IMP_FORALL_THM : thm
val LE_1 : thm
val LE_C : thm
val LE_CASES : thm
val LE_SUC_LT : thm
val LT : thm
val LT_CASES : thm
val LT_LE : thm
val LT_NZ : thm
val LT_SUC_LE : thm
val NUM_COUNTABLE : thm
val OR_EXISTS_THM : thm
val POW_EQ_X_EXP_X : thm
val POW_TWO_set_exp : thm
val RIGHT_IMP_EXISTS_THM : thm
val RIGHT_IMP_FORALL_THM : thm
val SET_SQUARED_CARDEQ_SET : thm
val SET_SUM_CARDEQ_SET : thm
val SING_SUBSET : thm
val SING_set_exp : thm
val SING_set_exp_CARD : thm
val SUBSET_CARDLEQ : thm
val SURJECTIVE_IFF_INJECTIVE : thm
val SURJECTIVE_IFF_INJECTIVE_GEN : thm
val SURJECTIVE_IMAGE : thm
val SURJECTIVE_IMAGE_THM : thm
val SURJECTIVE_ON_IMAGE : thm
val SURJECTIVE_ON_RIGHT_INVERSE : thm
val SURJECTIVE_RIGHT_INVERSE : thm
val UNION_ACI : thm
val UNION_LE_ADD_C : thm
val UNIV_list : thm
val bijections_cardeq : thm
val cardeq_INSERT : thm
val cardeq_REFL : thm
val cardeq_SYM : thm
val cardeq_TRANS : thm
val cardeq_bijns_cong : thm
val cardleq_ANTISYM : thm
val cardleq_REFL : thm
val cardleq_SURJ : thm
val cardleq_TRANS : thm
val cardleq_dichotomy : thm
val cardleq_empty : thm
val cardleq_lt_trans : thm
val cardleq_lteq : thm
val cardlt_REFL : thm
val cardlt_TRANS : thm
val cardlt_cardle : thm
val cardlt_lenoteq : thm
val cardlt_leq_trans : thm
val count_cardle : thm
val countable_cardeq : thm
val countable_decomposition : thm
val countable_thm : thm
val disjoint_countable_decomposition : thm
val eq_c : thm
val exp_INSERT_cardeq : thm
val exp_count_cardeq : thm
val finite_subsets_bijection : thm
val ge_c : thm
val gt_c : thm
val le_c : thm
val list_BIGUNION_EXP : thm
val list_EMPTY : thm
val list_SING : thm
val lt_c : thm
val mul_c : thm
val num_FINITE : thm
val num_FINITE_AVOID : thm
val num_INFINITE : thm
val set_binomial2 : thm
val set_exp_card_cong : thm
val set_exp_cardle_cong : thm
val set_exp_count : thm
val set_exp_product : thm
val cardinal_grammars : type_grammar.grammar * term_grammar.grammar
(*
[quotient] Parent theory of "cardinal"
[wellorder] Parent theory of "cardinal"
[add_c] Definition
⊢ ∀s t. s + t = {INL x | x ∈ s} ∪ {INR y | y ∈ t}
[bijns_def] Definition
⊢ ∀A. bijns A =
{f | THE ∘ f PERMUTES A ∧ ∀a. a ∈ A ⇔ ∃b. f a = SOME b}
[cardeq_def] Definition
⊢ ∀s1 s2. s1 ≈ s2 ⇔ ∃f. BIJ f s1 s2
[cardgeq_def] Definition
⊢ ∀s t. s ≽ t ⇔ t ≼ s
[cardgt_def] Definition
⊢ ∀s t. s ≻ t ⇔ t ≺ s
[cardleq_def] Definition
⊢ ∀s1 s2. s1 ≼ s2 ⇔ ∃f. INJ f s1 s2
[list_def] Definition
⊢ ∀A. list A = {l | ∀e. MEM e l ⇒ e ∈ A}
[set_exp_def] Definition
⊢ ∀A B.
A ** B =
{f |
(∀b. b ∈ B ⇒ ∃a. a ∈ A ∧ f b = SOME a) ∧ ∀b. b ∉ B ⇒ f b = NONE}
[BIJECTIVE_INJECTIVE_SURJECTIVE] Theorem
⊢ ∀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
[BIJECTIVE_INVERSES] Theorem
⊢ ∀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
[BIJ_functions_agree] Theorem
⊢ ∀f g s t. BIJ f s t ∧ (∀x. x ∈ s ⇒ f x = g x) ⇒ BIJ g s t
[CANTOR] Theorem
⊢ A ≺ POW A
[CANTOR_THM] Theorem
⊢ ∀s. s ≺ {t | t ⊆ s}
[CANTOR_THM_UNIV] Theorem
⊢ 𝕌(:α) ≺ 𝕌(:α -> bool)
[CARDEQ_0] Theorem
⊢ (x ≈ ∅ ⇔ x = ∅) ∧ (∅ ≈ x ⇔ x = ∅)
[CARDEQ_CARD] Theorem
⊢ s1 ≈ s2 ∧ FINITE s1 ⇒ CARD s1 = CARD s2
[CARDEQ_CARDLEQ] Theorem
⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)
[CARDEQ_CARD_EQN] Theorem
⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≈ s2 ⇔ CARD s1 = CARD s2)
[CARDEQ_CROSS] Theorem
⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2
[CARDEQ_CROSS_SYM] Theorem
⊢ s × t ≈ t × s
[CARDEQ_FINITE] Theorem
⊢ s1 ≈ s2 ⇒ (FINITE s1 ⇔ FINITE s2)
[CARDEQ_INSERT_RWT] Theorem
⊢ ∀s. INFINITE s ⇒ x INSERT s ≈ s
[CARDEQ_SUBSET_CARDLEQ] Theorem
⊢ s ≈ t ⇒ s ≼ t
[CARDLEQ_CARD] Theorem
⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≼ s2 ⇔ CARD s1 ≤ CARD s2)
[CARDLEQ_CROSS_CONG] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2
[CARDLEQ_FINITE] Theorem
⊢ ∀s1 s2. FINITE s2 ∧ s1 ≼ s2 ⇒ FINITE s1
[CARD_ADD2_ABSORB_LE] Theorem
⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s + t ≼ u
[CARD_ADD2_ABSORB_LT] Theorem
⊢ ∀s t u. INFINITE u ∧ s ≺ u ∧ t ≺ u ⇒ s + t ≺ u
[CARD_ADD_ABSORB] Theorem
⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s + t ≈ t
[CARD_ADD_ABSORB_LE] Theorem
⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s + t ≼ t
[CARD_ADD_ASSOC] Theorem
⊢ ∀s t u. s + (t + u) ≈ s + t + u
[CARD_ADD_C] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ CARD (s + t) = CARD s + CARD t
[CARD_ADD_CONG] Theorem
⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ s + t ≈ s' + t'
[CARD_ADD_FINITE] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE (s + t)
[CARD_ADD_FINITE_EQ] Theorem
⊢ ∀s t. FINITE (s + t) ⇔ FINITE s ∧ FINITE t
[CARD_ADD_LE_MUL_INFINITE] Theorem
⊢ ∀s. INFINITE s ⇒ s + s ≼ s × s
[CARD_ADD_SYM] Theorem
⊢ ∀s t. s + t ≈ t + s
[CARD_BIGUNION] Theorem
⊢ INFINITE k ∧ s1 ≼ k ∧ (∀e. e ∈ s1 ⇒ e ≼ k) ⇒ BIGUNION s1 ≼ k
[CARD_BIGUNION_LE] Theorem
⊢ ∀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_BOOL] Theorem
⊢ CARD 𝕌(:bool) = 2
[CARD_CARDEQ_I] Theorem
⊢ FINITE s1 ∧ FINITE s2 ∧ CARD s1 = CARD s2 ⇒ s1 ≈ s2
[CARD_CART_UNIV] Theorem
⊢ FINITE 𝕌(:α) ⇒ CARD 𝕌(:α) = CARD 𝕌(:α) ** 1
[CARD_COUNTABLE_CONG] Theorem
⊢ ∀s t. s ≈ t ⇒ (COUNTABLE s ⇔ COUNTABLE t)
[CARD_DISJOINT_UNION] Theorem
⊢ ∀s t. s ∩ t = ∅ ⇒ s ∪ t ≈ s + t
[CARD_EQ_BIJECTION] Theorem
⊢ ∀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_EQ_BIJECTIONS] Theorem
⊢ ∀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_CARD] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≈ t ⇔ CARD s = CARD t)
[CARD_EQ_CARD_IMP] Theorem
⊢ ∀s t. FINITE t ∧ s ≈ t ⇒ CARD s = CARD t
[CARD_EQ_CONG] Theorem
⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≈ t ⇔ s' ≈ t')
[CARD_EQ_COUNTABLE] Theorem
⊢ ∀s t. COUNTABLE t ∧ s ≈ t ⇒ COUNTABLE s
[CARD_EQ_EMPTY] Theorem
⊢ ∀s. s ≈ ∅ ⇔ s = ∅
[CARD_EQ_FINITE] Theorem
⊢ ∀s t. FINITE t ∧ s ≈ t ⇒ FINITE s
[CARD_EQ_IMAGE] Theorem
⊢ ∀f s. (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒ IMAGE f s ≈ s
[CARD_EQ_IMP_LE] Theorem
⊢ ∀s t. s ≈ t ⇒ s ≼ t
[CARD_EQ_REFL] Theorem
⊢ ∀s. s ≈ s
[CARD_EQ_SYM] Theorem
⊢ ∀s t. s ≈ t ⇔ t ≈ s
[CARD_EQ_TRANS] Theorem
⊢ ∀s t u. s ≈ t ∧ t ≈ u ⇒ s ≈ u
[CARD_FINITE_CONG] Theorem
⊢ ∀s t. s ≈ t ⇒ (FINITE s ⇔ FINITE t)
[CARD_HAS_SIZE_CONG] Theorem
⊢ ∀s t n. s HAS_SIZE n ∧ s ≈ t ⇒ t HAS_SIZE n
[CARD_IMAGE_INJ] Theorem
⊢ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ∧ FINITE s ⇒
CARD (IMAGE f s) = CARD s
[CARD_IMAGE_LE] Theorem
⊢ ∀f s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s
[CARD_INFINITE_CONG] Theorem
⊢ ∀s t. s ≈ t ⇒ (INFINITE s ⇔ INFINITE t)
[CARD_LDISTRIB] Theorem
⊢ ∀s t u. s × (t + u) ≈ s × t + s × u
[CARD_LET_TOTAL] Theorem
⊢ ∀s t. s ≼ t ∨ t ≺ s
[CARD_LET_TRANS] Theorem
⊢ ∀s t u. s ≼ t ∧ t ≺ u ⇒ s ≺ u
[CARD_LE_ADD] Theorem
⊢ ∀s s' t t'. s ≼ s' ∧ t ≼ t' ⇒ s + t ≼ s' + t'
[CARD_LE_ADDL] Theorem
⊢ ∀s t. t ≼ s + t
[CARD_LE_ADDR] Theorem
⊢ ∀s t. s ≼ s + t
[CARD_LE_ANTISYM] Theorem
⊢ ∀s t. s ≼ t ∧ t ≼ s ⇔ s ≈ t
[CARD_LE_CARD] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≼ t ⇔ CARD s ≤ CARD t)
[CARD_LE_CARD_IMP] Theorem
⊢ ∀s t. FINITE t ∧ s ≼ t ⇒ CARD s ≤ CARD t
[CARD_LE_CONG] Theorem
⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≼ t ⇔ s' ≼ t')
[CARD_LE_COUNTABLE] Theorem
⊢ ∀s t. COUNTABLE t ∧ s ≼ t ⇒ COUNTABLE s
[CARD_LE_EMPTY] Theorem
⊢ ∀s. s ≼ ∅ ⇔ s = ∅
[CARD_LE_EQ_SUBSET] Theorem
⊢ ∀s t. s ≼ t ⇔ ∃u. u ⊆ t ∧ s ≈ u
[CARD_LE_FINITE] Theorem
⊢ ∀s t. FINITE t ∧ s ≼ t ⇒ FINITE s
[CARD_LE_IMAGE] Theorem
⊢ ∀f s. IMAGE f s ≼ s
[CARD_LE_IMAGE_GEN] Theorem
⊢ ∀f s t. t ⊆ IMAGE f s ⇒ t ≼ s
[CARD_LE_INFINITE] Theorem
⊢ ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t
[CARD_LE_INJ] Theorem
⊢ ∀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_LT] Theorem
⊢ ∀s t. s ≼ t ⇔ s ≺ t ∨ s ≈ t
[CARD_LE_MUL] Theorem
⊢ ∀s s' t t'. s ≼ s' ∧ t ≼ t' ⇒ s × t ≼ s' × t'
[CARD_LE_REFL] Theorem
⊢ ∀s. s ≼ s
[CARD_LE_RELATIONAL] Theorem
⊢ ∀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_SQUARE] Theorem
⊢ ∀s. s ≼ s × s
[CARD_LE_SUBSET] Theorem
⊢ ∀s t. s ⊆ t ⇒ s ≼ t
[CARD_LE_TOTAL] Theorem
⊢ ∀s t. s ≼ t ∨ t ≼ s
[CARD_LE_TRANS] Theorem
⊢ ∀s t u. s ≼ t ∧ t ≼ u ⇒ s ≼ u
[CARD_LE_UNIV] Theorem
⊢ ∀s. s ≼ 𝕌(:α)
[CARD_LTE_TOTAL] Theorem
⊢ ∀s t. s ≺ t ∨ t ≼ s
[CARD_LTE_TRANS] Theorem
⊢ ∀s t u. s ≺ t ∧ t ≼ u ⇒ s ≺ u
[CARD_LT_ADD] Theorem
⊢ ∀s s' t t'. s ≺ s' ∧ t ≺ t' ⇒ s + t ≺ s' + t'
[CARD_LT_CARD] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s ≺ t ⇔ CARD s < CARD t)
[CARD_LT_CONG] Theorem
⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ (s ≺ t ⇔ s' ≺ t')
[CARD_LT_FINITE_INFINITE] Theorem
⊢ ∀s t. FINITE s ∧ INFINITE t ⇒ s ≺ t
[CARD_LT_IMP_LE] Theorem
⊢ ∀s t. s ≺ t ⇒ s ≼ t
[CARD_LT_LE] Theorem
⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ ¬(s ≈ t)
[CARD_LT_REFL] Theorem
⊢ ∀s. ¬(s ≺ s)
[CARD_LT_TOTAL] Theorem
⊢ ∀s t. s ≈ t ∨ s ≺ t ∨ t ≺ s
[CARD_LT_TRANS] Theorem
⊢ ∀s t u. s ≺ t ∧ t ≺ u ⇒ s ≺ u
[CARD_MUL2_ABSORB_LE] Theorem
⊢ ∀s t u. INFINITE u ∧ s ≼ u ∧ t ≼ u ⇒ s × t ≼ u
[CARD_MUL_ABSORB] Theorem
⊢ ∀s t. INFINITE t ∧ s ≠ ∅ ∧ s ≼ t ⇒ s × t ≈ t
[CARD_MUL_ABSORB_LE] Theorem
⊢ ∀s t. INFINITE t ∧ s ≼ t ⇒ s × t ≼ t
[CARD_MUL_ASSOC] Theorem
⊢ ∀s t u. s × (t × u) ≈ s × t × u
[CARD_MUL_CONG] Theorem
⊢ ∀s s' t t'. s ≈ s' ∧ t ≈ t' ⇒ s × t ≈ s' × t'
[CARD_MUL_FINITE] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE (s × t)
[CARD_MUL_LT_INFINITE] Theorem
⊢ ∀s t u. s ≺ u ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u
[CARD_MUL_LT_LEMMA] Theorem
⊢ ∀s t u. s ≼ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u
[CARD_MUL_SYM] Theorem
⊢ ∀s t. s × t ≈ t × s
[CARD_NOT_LE] Theorem
⊢ ∀s t. t ≺ s ⇔ t ≺ s
[CARD_NOT_LT] Theorem
⊢ ∀s t. ¬(s ≺ t) ⇔ t ≼ s
[CARD_RDISTRIB] Theorem
⊢ ∀s t u. (s + t) × u ≈ s × u + t × u
[CARD_SQUARE_INFINITE] Theorem
⊢ ∀s. INFINITE s ⇒ s × s ≈ s
[CARD_SQUARE_NUM] Theorem
⊢ 𝕌(:num) × 𝕌(:num) ≈ 𝕌(:num)
[CARD_SUBSET_EQ] Theorem
⊢ ∀a b. FINITE b ∧ a ⊆ b ∧ CARD a = CARD b ⇒ a = b
[CONJ_ACI] Theorem
⊢ ∀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)
[CONJ_EQ_IMP] Theorem
⊢ ∀p q r. p ∧ q ⇒ r ⇔ p ⇒ q ⇒ r
[COUNTABLE] Theorem
⊢ ∀t. COUNTABLE t ⇔ 𝕌(:num) ≽ t
[COUNTABLE_ALT_cardleq] Theorem
⊢ ∀s. COUNTABLE s ⇔ s ≼ 𝕌(:num)
[COUNTABLE_AS_IMAGE] Theorem
⊢ ∀s. COUNTABLE s ∧ s ≠ ∅ ⇒ ∃f. s = IMAGE f 𝕌(:num)
[COUNTABLE_AS_IMAGE_SUBSET] Theorem
⊢ ∀s. COUNTABLE s ⇒ ∃f. s ⊆ IMAGE f 𝕌(:num)
[COUNTABLE_AS_IMAGE_SUBSET_EQ] Theorem
⊢ ∀s. COUNTABLE s ⇔ ∃f. s ⊆ IMAGE f 𝕌(:num)
[COUNTABLE_AS_INJECTIVE_IMAGE] Theorem
⊢ ∀s. COUNTABLE s ∧ INFINITE s ⇒
∃f. s = IMAGE f 𝕌(:num) ∧ ∀m n. f m = f n ⇒ m = n
[COUNTABLE_BIGUNION] Theorem
⊢ ∀A. COUNTABLE A ∧ (∀s. s ∈ A ⇒ COUNTABLE s) ⇒
COUNTABLE (BIGUNION A)
[COUNTABLE_CASES] Theorem
⊢ ∀s. COUNTABLE s ⇔ FINITE s ∨ s ≈ 𝕌(:num)
[COUNTABLE_CROSS] Theorem
⊢ ∀s t. COUNTABLE s ∧ COUNTABLE t ⇒ COUNTABLE (s × t)
[COUNTABLE_DELETE] Theorem
⊢ ∀x s. COUNTABLE (s DELETE x) ⇔ COUNTABLE s
[COUNTABLE_DIFF_FINITE] Theorem
⊢ ∀s t. FINITE s ⇒ (COUNTABLE (t DIFF s) ⇔ COUNTABLE t)
[COUNTABLE_EMPTY] Theorem
⊢ COUNTABLE ∅
[COUNTABLE_IMAGE] Theorem
⊢ ∀f s. COUNTABLE s ⇒ COUNTABLE (IMAGE f s)
[COUNTABLE_IMAGE_INJ] Theorem
⊢ ∀f A.
(∀x y. f x = f y ⇒ x = y) ∧ COUNTABLE A ⇒ COUNTABLE {x | f x ∈ A}
[COUNTABLE_IMAGE_INJ_EQ] Theorem
⊢ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
(COUNTABLE (IMAGE f s) ⇔ COUNTABLE s)
[COUNTABLE_IMAGE_INJ_GENERAL] Theorem
⊢ ∀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_INSERT] Theorem
⊢ ∀x s. COUNTABLE (x INSERT s) ⇔ COUNTABLE s
[COUNTABLE_INTER] Theorem
⊢ ∀s t. COUNTABLE s ∨ COUNTABLE t ⇒ COUNTABLE (s ∩ t)
[COUNTABLE_PRODUCT_DEPENDENT] Theorem
⊢ ∀f s t.
COUNTABLE s ∧ (∀x. x ∈ s ⇒ COUNTABLE (t x)) ⇒
COUNTABLE {f x y | x ∈ s ∧ y ∈ t x}
[COUNTABLE_RESTRICT] Theorem
⊢ ∀s P. COUNTABLE s ⇒ COUNTABLE {x | x ∈ s ∧ P x}
[COUNTABLE_SING] Theorem
⊢ ∀x. COUNTABLE {x}
[COUNTABLE_UNION] Theorem
⊢ ∀s t. COUNTABLE (s ∪ t) ⇔ COUNTABLE s ∧ COUNTABLE t
[COUNTABLE_UNION_IMP] Theorem
⊢ ∀s t. COUNTABLE s ∧ COUNTABLE t ⇒ COUNTABLE (s ∪ t)
[COUNT_EQ_EMPTY] Theorem
⊢ count n = ∅ ⇔ n = 0
[EMPTY_CARDLEQ] Theorem
⊢ ∅ ≼ t
[EMPTY_set_exp] Theorem
⊢ A ** ∅ = {K NONE} ∧ (B ≠ ∅ ⇒ ∅ ** B = ∅)
[EMPTY_set_exp_CARD] Theorem
⊢ A ** ∅ ≈ count 1
[EQ_C] Theorem
⊢ ∀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)
[FINITE_BOOL] Theorem
⊢ FINITE 𝕌(:bool)
[FINITE_CARD_LT] Theorem
⊢ ∀s. FINITE s ⇔ s ≺ 𝕌(:num)
[FINITE_CART_UNIV] Theorem
⊢ FINITE 𝕌(:α) ⇒ FINITE 𝕌(:α)
[FINITE_CLE_INFINITE] Theorem
⊢ FINITE s ∧ INFINITE t ⇒ s ≼ t
[FINITE_FINITE_BIGUNION] Theorem
⊢ ∀s. FINITE s ⇒ (FINITE (BIGUNION s) ⇔ ∀t. t ∈ s ⇒ FINITE t)
[FINITE_FINITE_BIGUNIONS] Theorem
⊢ ∀s. FINITE s ⇒ (FINITE (BIGUNION s) ⇔ ∀t. t ∈ s ⇒ FINITE t)
[FINITE_IMAGE_INJ] Theorem
⊢ ∀f A. (∀x y. f x = f y ⇒ x = y) ∧ FINITE A ⇒ FINITE {x | f x ∈ A}
[FINITE_IMAGE_INJ'] Theorem
⊢ (∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y ⇔ x = y)) ⇒
(FINITE (IMAGE f s) ⇔ FINITE s)
[FINITE_IMAGE_INJ_EQ] Theorem
⊢ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
(FINITE (IMAGE f s) ⇔ FINITE s)
[FINITE_IMAGE_INJ_GENERAL] Theorem
⊢ ∀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_IMP_COUNTABLE] Theorem
⊢ ∀s. FINITE s ⇒ COUNTABLE s
[FINITE_NUMSEG_LE] Theorem
⊢ ∀n. FINITE {m | m ≤ n}
[FINITE_NUMSEG_LT] Theorem
⊢ ∀n. FINITE {m | m < n}
[FINITE_PRODUCT] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE {(x,y) | x ∈ s ∧ y ∈ t}
[FINITE_PRODUCT_DEPENDENT] Theorem
⊢ ∀f s t.
FINITE s ∧ (∀x. x ∈ s ⇒ FINITE (t x)) ⇒
FINITE {f x y | x ∈ s ∧ y ∈ t x}
[FORALL_COUNTABLE_AS_IMAGE] Theorem
⊢ (∀d. COUNTABLE d ⇒ P d) ⇔ P ∅ ∧ ∀f. P (IMAGE f 𝕌(:num))
[GE] Theorem
⊢ ∀n m. m ≥ n ⇔ n ≤ m
[GE_C] Theorem
⊢ ∀s t. s ≽ t ⇔ ∃f. ∀y. y ∈ t ⇒ ∃x. x ∈ s ∧ y = f x
[HAS_SIZE_BOOL] Theorem
⊢ 𝕌(:bool) HAS_SIZE 2
[HAS_SIZE_CART_UNIV] Theorem
⊢ ∀m. 𝕌(:α) HAS_SIZE m ⇒ 𝕌(:α) HAS_SIZE m ** 1
[HAS_SIZE_CLAUSES] Theorem
⊢ ∀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_INDEX] Theorem
⊢ ∀s n.
s HAS_SIZE n ⇒
∃f. (∀m. m < n ⇒ f m ∈ s) ∧ ∀x. x ∈ s ⇒ ∃!m. m < n ∧ f m = x
[HAS_SIZE_NUMSEG_LE] Theorem
⊢ ∀n. {m | m ≤ n} HAS_SIZE n + 1
[HAS_SIZE_NUMSEG_LT] Theorem
⊢ ∀n. {m | m < n} HAS_SIZE n
[IMAGE_cardleq] Theorem
⊢ ∀f s. IMAGE f s ≼ s
[IMAGE_cardleq_rwt] Theorem
⊢ ∀s t. s ≼ t ⇒ IMAGE f s ≼ t
[IMP_CONJ_ALT] Theorem
⊢ ∀p q r. p ∧ q ⇒ r ⇔ q ⇒ p ⇒ r
[INFINITE_A_list_BIJ_A] Theorem
⊢ INFINITE A ⇒ list A ≈ A
[INFINITE_CARD_LE] Theorem
⊢ ∀s. INFINITE s ⇔ 𝕌(:num) ≼ s
[INFINITE_DIFF_FINITE] Theorem
⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ INFINITE (s DIFF t)
[INFINITE_IMAGE_INJ] Theorem
⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒
∀s. INFINITE s ⇒ INFINITE (IMAGE f s)
[INFINITE_NONEMPTY] Theorem
⊢ ∀s. INFINITE s ⇒ s ≠ ∅
[INFINITE_UNIV_INF] Theorem
⊢ INFINITE 𝕌(:num + α)
[INFINITE_Unum] Theorem
⊢ INFINITE A ⇔ 𝕌(:num) ≼ A
[INFINITE_cardleq_INSERT] Theorem
⊢ INFINITE A ⇒ (x INSERT s ≼ A ⇔ s ≼ A)
[INJECTIVE_IMAGE] Theorem
⊢ ∀f. (∀s t. IMAGE f s = IMAGE f t ⇒ s = t) ⇔ ∀x y. f x = f y ⇒ x = y
[INJECTIVE_LEFT_INVERSE] Theorem
⊢ (∀x y. f x = f y ⇒ x = y) ⇔ ∃g. ∀x. g (f x) = x
[INJECTIVE_ON_IMAGE] Theorem
⊢ ∀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_ON_LEFT_INVERSE] Theorem
⊢ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇔
∃g. ∀x. x ∈ s ⇒ g (f x) = x
[INTER_ACI] Theorem
⊢ ∀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
[IN_CARD_ADD] Theorem
⊢ (∀x. INL x ∈ s + t ⇔ x ∈ s) ∧ ∀y. INR y ∈ s + t ⇔ y ∈ t
[IN_CARD_MUL] Theorem
⊢ ∀s t x y. (x,y) ∈ s × t ⇔ x ∈ s ∧ y ∈ t
[IN_ELIM_PAIR_THM] Theorem
⊢ ∀P a b. (a,b) ∈ {(x,y) | P x y} ⇔ P a b
[LEFT_IMP_EXISTS_THM] Theorem
⊢ ∀P Q. (∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q
[LEFT_IMP_FORALL_THM] Theorem
⊢ ∀P Q. (∀x. P x) ⇒ Q ⇔ ∃x. P x ⇒ Q
[LE_1] Theorem
⊢ (∀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
[LE_C] Theorem
⊢ ∀s t. s ≼ t ⇔ ∃g. ∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ g y = x
[LE_CASES] Theorem
⊢ ∀m n. m ≤ n ∨ n ≤ m
[LE_SUC_LT] Theorem
⊢ ∀m n. SUC m ≤ n ⇔ m < n
[LT] Theorem
⊢ (∀m. m < 0 ⇔ F) ∧ ∀m n. m < SUC n ⇔ m = n ∨ m < n
[LT_CASES] Theorem
⊢ ∀m n. m < n ∨ n < m ∨ m = n
[LT_LE] Theorem
⊢ ∀m n. m < n ⇔ m ≤ n ∧ m ≠ n
[LT_NZ] Theorem
⊢ ∀n. 0 < n ⇔ n ≠ 0
[LT_SUC_LE] Theorem
⊢ ∀m n. m < SUC n ⇔ m ≤ n
[NUM_COUNTABLE] Theorem
⊢ COUNTABLE 𝕌(:num)
[OR_EXISTS_THM] Theorem
⊢ ∀P Q. (∃x. P x) ∨ (∃x. Q x) ⇔ ∃x. P x ∨ Q x
[POW_EQ_X_EXP_X] Theorem
⊢ INFINITE A ⇒ POW A ≈ A ** A
[POW_TWO_set_exp] Theorem
⊢ POW A ≈ count 2 ** A
[RIGHT_IMP_EXISTS_THM] Theorem
⊢ ∀P Q. P ⇒ (∃x. Q x) ⇔ ∃x. P ⇒ Q x
[RIGHT_IMP_FORALL_THM] Theorem
⊢ ∀P Q. P ⇒ (∀x. Q x) ⇔ ∀x. P ⇒ Q x
[SET_SQUARED_CARDEQ_SET] Theorem
⊢ ∀s. INFINITE s ⇒ s × s ≈ s
[SET_SUM_CARDEQ_SET] Theorem
⊢ INFINITE s ⇒
s ≈ {T; F} × s ∧ ∀A B. DISJOINT A B ∧ A ≈ s ∧ B ≈ s ⇒ A ∪ B ≈ s
[SING_SUBSET] Theorem
⊢ ∀s x. {x} ⊆ s ⇔ x ∈ s
[SING_set_exp] Theorem
⊢ {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] Theorem
⊢ {x} ** B ≈ count 1 ∧ A ** {x} ≈ A
[SUBSET_CARDLEQ] Theorem
⊢ ∀x y. x ⊆ y ⇒ x ≼ y
[SURJECTIVE_IFF_INJECTIVE] Theorem
⊢ ∀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)
[SURJECTIVE_IFF_INJECTIVE_GEN] Theorem
⊢ ∀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_IMAGE] Theorem
⊢ ∀f. (∀t. ∃s. IMAGE f s = t) ⇔ ∀y. ∃x. f x = y
[SURJECTIVE_IMAGE_THM] Theorem
⊢ ∀f. (∀y. ∃x. f x = y) ⇔ ∀P. IMAGE f {x | P (f x)} = {x | P x}
[SURJECTIVE_ON_IMAGE] Theorem
⊢ ∀f u v.
(∀t. t ⊆ v ⇒ ∃s. s ⊆ u ∧ IMAGE f s = t) ⇔
∀y. y ∈ v ⇒ ∃x. x ∈ u ∧ f x = y
[SURJECTIVE_ON_RIGHT_INVERSE] Theorem
⊢ ∀f t.
(∀y. y ∈ t ⇒ ∃x. x ∈ s ∧ f x = y) ⇔
∃g. ∀y. y ∈ t ⇒ g y ∈ s ∧ f (g y) = y
[SURJECTIVE_RIGHT_INVERSE] Theorem
⊢ (∀y. ∃x. f x = y) ⇔ ∃g. ∀y. f (g y) = y
[UNION_ACI] Theorem
⊢ ∀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
[UNION_LE_ADD_C] Theorem
⊢ ∀s t. s ∪ t ≼ s + t
[UNIV_list] Theorem
⊢ 𝕌(:α list) = list 𝕌(:α)
[bijections_cardeq] Theorem
⊢ INFINITE s ⇒ bijns s ≈ POW s
[cardeq_INSERT] Theorem
⊢ x INSERT s ≈ s ⇔ x ∈ s ∨ INFINITE s
[cardeq_REFL] Theorem
⊢ ∀s. s ≈ s
[cardeq_SYM] Theorem
⊢ ∀s t. s ≈ t ⇔ t ≈ s
[cardeq_TRANS] Theorem
⊢ ∀s t u. s ≈ t ∧ t ≈ u ⇒ s ≈ u
[cardeq_bijns_cong] Theorem
⊢ A ≈ B ⇒ bijns A ≈ bijns B
[cardleq_ANTISYM] Theorem
⊢ ∀s t. s ≼ t ∧ t ≼ s ⇒ s ≈ t
[cardleq_REFL] Theorem
⊢ ∀s. s ≼ s
[cardleq_SURJ] Theorem
⊢ A ≼ B ⇔ (∃f. SURJ f B A) ∨ A = ∅
[cardleq_TRANS] Theorem
⊢ ∀s t u. s ≼ t ∧ t ≼ u ⇒ s ≼ u
[cardleq_dichotomy] Theorem
⊢ ∀s t. s ≼ t ∨ t ≼ s
[cardleq_empty] Theorem
⊢ ∀x. x ≼ ∅ ⇔ x = ∅
[cardleq_lt_trans] Theorem
⊢ ∀r s t. r ≼ s ∧ s ≺ t ⇒ r ≺ t
[cardleq_lteq] Theorem
⊢ ∀s1 s2. s1 ≼ s2 ⇔ s1 ≺ s2 ∨ s1 ≈ s2
[cardlt_REFL] Theorem
⊢ ∀s. ¬(s ≺ s)
[cardlt_TRANS] Theorem
⊢ ∀s t u. s ≺ t ∧ t ≺ u ⇒ s ≺ u
[cardlt_cardle] Theorem
⊢ A ≺ B ⇒ A ≼ B
[cardlt_lenoteq] Theorem
⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ ¬(s ≈ t)
[cardlt_leq_trans] Theorem
⊢ ∀r s t. r ≺ s ∧ s ≼ t ⇒ r ≺ t
[count_cardle] Theorem
⊢ count n ≼ A ⇔ FINITE A ⇒ n ≤ CARD A
[countable_cardeq] Theorem
⊢ ∀s t. s ≈ t ⇒ (COUNTABLE s ⇔ COUNTABLE t)
[countable_decomposition] Theorem
⊢ ∀s. INFINITE s ⇒
∃A. BIGUNION A = s ∧ ∀a. a ∈ A ⇒ INFINITE a ∧ COUNTABLE a
[countable_thm] Theorem
⊢ ∀s. COUNTABLE s ⇔ s ≼ 𝕌(:num)
[disjoint_countable_decomposition] Theorem
⊢ ∀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
[eq_c] Theorem
⊢ ∀s t.
s ≈ t ⇔
∃f. (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ f x = y
[exp_INSERT_cardeq] Theorem
⊢ e ∉ s ⇒ A ** (e INSERT s) ≈ A × A ** s
[exp_count_cardeq] Theorem
⊢ INFINITE A ∧ 0 < n ⇒ A ** count n ≈ A
[finite_subsets_bijection] Theorem
⊢ INFINITE A ⇒ A ≈ {s | FINITE s ∧ s ⊆ A}
[ge_c] Theorem
⊢ ∀s t. s ≽ t ⇔ t ≼ s
[gt_c] Theorem
⊢ ∀s t. s ≻ t ⇔ t ≺ s
[le_c] Theorem
⊢ ∀s t.
s ≼ t ⇔
∃f. (∀x. x ∈ s ⇒ f x ∈ t) ∧
∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y
[list_BIGUNION_EXP] Theorem
⊢ list A ≈ BIGUNION (IMAGE (λn. A ** count n) 𝕌(:num))
[list_EMPTY] Theorem
⊢ list ∅ = {[]}
[list_SING] Theorem
⊢ list {e} ≈ 𝕌(:num)
[lt_c] Theorem
⊢ ∀s t. s ≺ t ⇔ s ≼ t ∧ s ≺ t
[mul_c] Theorem
⊢ ∀s t. s × t = {(x,y) | x ∈ s ∧ y ∈ t}
[num_FINITE] Theorem
⊢ ∀s. FINITE s ⇔ ∃a. ∀x. x ∈ s ⇒ x ≤ a
[num_FINITE_AVOID] Theorem
⊢ ∀s. FINITE s ⇒ ∃a. a ∉ s
[num_INFINITE] Theorem
⊢ INFINITE 𝕌(:num)
[set_binomial2] Theorem
⊢ (A ∪ B) × (A ∪ B) = A × A ∪ A × B ∪ B × A ∪ B × B
[set_exp_card_cong] Theorem
⊢ a1 ≈ a2 ⇒ b1 ≈ b2 ⇒ a1 ** b1 ≈ a2 ** b2
[set_exp_cardle_cong] Theorem
⊢ (b = ∅ ⇒ d = ∅) ⇒ a ≼ b ∧ c ≼ d ⇒ a ** c ≼ b ** d
[set_exp_count] Theorem
⊢ A ** count n ≈ {l | LENGTH l = n ∧ ∀e. MEM e l ⇒ e ∈ A}
[set_exp_product] Theorem
⊢ (A ** B1) ** B2 ≈ A ** (B1 × B2)
*)
end
HOL 4, Kananaskis-14