Structure cardinalTheory
signature cardinalTheory =
sig
type thm = Thm.thm
(* Definitions *)
val BIGPROD_def : thm
val BIGPRODi_def : thm
val bijns_def : thm
val cardeq_def : thm
val cardgeq_def : thm
val cardgt_def : thm
val cardleq_def : thm
val fnOfSet_def : thm
val list_def : thm
val set_exp_def : thm
(* Theorems *)
val BIGPROD_CONS : thm
val BIGPROD_EQ_EMPTY : thm
val BIGPROD_ONE : thm
val BIGPROD_SING : thm
val BIGPROD_pair : thm
val BIGPROD_thm : thm
val BIGPRODi_11 : thm
val BIGPRODi_EQ_EMPTY : thm
val BIGPRODi_KNONE : thm
val BIGPRODi_SING_CEQ : thm
val BIGPRODi_SING_EQ : thm
val BIGPRODi_pair : thm
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 CARD1_SING : 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_1 : thm
val CARDEQ_CROSS_SYM : thm
val CARDEQ_DISJOINT_UNION : 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_12 : 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_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_EXP : 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 EXISTS_IN_GSPEC : thm
val FINITE_012 : thm
val FINITE_BOOL : thm
val FINITE_CARD_LT : thm
val FINITE_CART_UNIV : thm
val FINITE_CLE_INFINITE : thm
val FINITE_EXPONENT_SETEXP_COUNTABLE : thm
val FINITE_EXPONENT_SETEXP_UNCOUNTABLE : 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 FINITE_setexp : thm
val FORALL_COUNTABLE_AS_IMAGE : thm
val FORALL_IN_GSPEC : 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_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_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_SUC_LT : thm
val LT_NZ : 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_fun_exp : 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_addUnum : thm
val cardeq_bijns_cong : thm
val cardleq_ANTISYM : thm
val cardleq_REFL : thm
val cardleq_SURJ : thm
val cardleq_TRANS : thm
val cardleq_copy_wellorders : thm
val cardleq_dichotomy : thm
val cardleq_empty : thm
val cardleq_lt_trans : thm
val cardleq_lteq : thm
val cardleq_setexp : 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_setexp : 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 fnOfSet_SING : 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 setexp_eq_EMPTY : thm
val tupNONE_IN_BIGPRODi : thm
val wellorder_destWO : thm
val cardinal_grammars : type_grammar.grammar * term_grammar.grammar
(*
[wellorder] Parent theory of "cardinal"
[BIGPROD_def] Definition
⊢ ∀A. BIGPROD A = BIGPRODi (λa. if a ∈ A then SOME a else NONE)
[BIGPRODi_def] Definition
⊢ ∀A. BIGPRODi A =
{tup |
(∀i. A i = NONE ⇒ tup i = NONE) ∧
∀i s. A i = SOME s ⇒ ∃a. tup i = SOME a ∧ a ∈ s}
[bijns_def] Definition
⊢ ∀A. bijns A = {f | f PERMUTES A ∧ ∀a. a ∉ A ⇒ f a = a}
[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
[fnOfSet_def] Definition
⊢ ∀s k.
fnOfSet s k =
if ∃!v. (k,v) ∈ s then SOME (@v. (k,v) ∈ s) else NONE
[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 = a) ∧ ∀b. b ∉ B ⇒ f b = ARB}
[BIGPROD_CONS] Theorem
⊢ A × BIGPROD As ≈ BIGPROD (IMAGE INL A INSERT IMAGE (IMAGE INR) As)
[BIGPROD_EQ_EMPTY] Theorem
⊢ BIGPROD As = ∅ ⇔ ∅ ∈ As
[BIGPROD_ONE] Theorem
⊢ BIGPROD ∅ ≈ 𝟙
[BIGPROD_SING] Theorem
⊢ BIGPROD {A} ≈ A
[BIGPROD_pair] Theorem
⊢ A1 ≠ A2 ⇒ BIGPROD {A1; A2} ≈ A1 × A2
[BIGPROD_thm] Theorem
⊢ BIGPROD A =
{tup |
(∀s. s ∈ A ⇒ ∃a. tup s = SOME a ∧ a ∈ s) ∧
∀s. s ∉ A ⇒ tup s = NONE}
[BIGPRODi_11] Theorem
⊢ (∀i. Af i ≠ SOME ∅) ∧ (∀i. Bf i ≠ SOME ∅) ⇒
(BIGPRODi Af = BIGPRODi Bf ⇔ Af = Bf)
[BIGPRODi_EQ_EMPTY] Theorem
⊢ BIGPRODi Af = ∅ ⇔ ∃i. Af i = SOME ∅
[BIGPRODi_KNONE] Theorem
⊢ BIGPRODi (K NONE) = {K NONE}
[BIGPRODi_SING_CEQ] Theorem
⊢ BIGPRODi (fnOfSet {(i,s)}) ≈ s
[BIGPRODi_SING_EQ] Theorem
⊢ BIGPRODi (fnOfSet {(i,s)}) = {(K NONE)⦇i ↦ SOME a⦈ | a ∈ s}
[BIGPRODi_pair] Theorem
⊢ i ≠ j ⇒ BIGPRODi (K NONE)⦇i ↦ SOME A1; j ↦ SOME A2⦈ ≈ A1 × A2
[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)
[CARD1_SING] Theorem
⊢ A ≈ 𝟙 ⇔ ∃a. A = {a}
[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_1] Theorem
⊢ {x} × A ≈ A ∧ A × {x} ≈ A
[CARDEQ_CROSS_SYM] Theorem
⊢ s × t ≈ t × s
[CARDEQ_DISJOINT_UNION] Theorem
⊢ ∀s t. s ∩ t = ∅ ⇒ s ∪ t ≈ s ⊔ t
[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_12] Theorem
⊢ 𝟙 ≺ 𝟚 ∧ 𝟙 ≉ 𝟚 ∧ 𝟚 ≉ 𝟙 ∧ 𝟙 ≼ 𝟚
[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
⊢ 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.
FINITE s ∧ FINITE t ∧ s ∩ t = ∅ ⇒ CARD (s ∪ t) = CARD s + CARD 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_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
⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ (s1 ≼ t1 ⇔ s2 ≼ t2)
[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_EXP] Theorem
⊢ 𝟚 ≼ B ⇒ A ≼ B ** A
[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
⊢ ∀s1 s2. s1 ≼ s2 ⇔ s1 ≺ s2 ∨ s1 ≈ s2
[CARD_LE_MUL] Theorem
⊢ ∀x1 x2 y1 y2. x1 ≼ x2 ∧ y1 ≼ y2 ⇒ x1 × y1 ≼ x2 × y2
[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
⊢ FINITE s1 ∧ FINITE s2 ⇒ (s1 ≺ s2 ⇔ CARD s1 < CARD s2)
[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
⊢ s1 ≈ s2 ∧ t1 ≈ t2 ⇒ s1 × t1 ≈ s2 × t2
[CARD_MUL_FINITE] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ FINITE (s × t)
[CARD_MUL_LT_INFINITE] Theorem
⊢ ∀s t. s ≺ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u
[CARD_MUL_LT_LEMMA] Theorem
⊢ ∀s t. s ≼ t ∧ t ≺ u ∧ INFINITE u ⇒ s × t ≺ u
[CARD_MUL_SYM] Theorem
⊢ 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
⊢ ∀s. countable s ∧ (∀x. x ∈ s ⇒ countable x) ⇒
countable (BIGUNION s)
[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 ARB} ∧ (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)
[EXISTS_IN_GSPEC] Theorem
⊢ (∀P f. (∃z. z ∈ {f x | P x} ∧ Q z) ⇔ ∃x. P x ∧ Q (f x)) ∧
(∀P f. (∃z. z ∈ {f x y | P x y} ∧ Q z) ⇔ ∃x y. P x y ∧ Q (f x y)) ∧
∀P f.
(∃z. z ∈ {f w x y | P w x y} ∧ Q z) ⇔
∃w x y. P w x y ∧ Q (f w x y)
[FINITE_012] Theorem
⊢ FINITE A ⇒ A = ∅ ∨ A ≈ 𝟙 ∨ 2 ≤ CARD A
[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_EXPONENT_SETEXP_COUNTABLE] Theorem
⊢ FINITE B ⇒ (countable (A ** B) ⇔ B = ∅ ∨ countable A)
[FINITE_EXPONENT_SETEXP_UNCOUNTABLE] Theorem
⊢ FINITE B ∧ B ≠ ∅ ∧ ¬countable A ⇒ ¬countable (A ** B)
[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}
[FINITE_setexp] Theorem
⊢ FINITE (A ** B) ⇔ B = ∅ ∨ A ≼ 𝟙 ∨ FINITE A ∧ FINITE B
[FORALL_COUNTABLE_AS_IMAGE] Theorem
⊢ (∀d. countable d ⇒ P d) ⇔ P ∅ ∧ ∀f. P (IMAGE f 𝕌(:num))
[FORALL_IN_GSPEC] Theorem
⊢ (∀P f. (∀z. z ∈ {f x | P x} ⇒ Q z) ⇔ ∀x. P x ⇒ Q (f x)) ∧
(∀P f. (∀z. z ∈ {f x y | P x y} ⇒ Q z) ⇔ ∀x y. P x y ⇒ Q (f x y)) ∧
∀P f.
(∀z. z ∈ {f w x y | P w x y} ⇒ Q z) ⇔
∀w x y. P w x y ⇒ Q (f w x y)
[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_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_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
⊢ (INL a ∈ A ⊔ B ⇔ a ∈ A) ∧ (INR b ∈ A ⊔ B ⇔ b ∈ B)
[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_SUC_LT] Theorem
⊢ ∀m n. SUC m ≤ n ⇔ m < n
[LT_NZ] Theorem
⊢ ∀n. 0 < n ⇔ n ≠ 0
[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 ≈ 𝟚 × 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 x else ARB)} ∧
A ** {x} = {(λb. if b = x then a else ARB) | 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_fun_exp] Theorem
⊢ 𝕌(:α -> β) = 𝕌(:β) ** 𝕌(:α)
[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_addUnum] Theorem
⊢ INFINITE 𝕌(:α) ⇒ 𝕌(:num + α) ≈ 𝕌(:α)
[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_copy_wellorders] Theorem
⊢ 𝕌(:α) ≼ 𝕌(:β) ⇒ ∀w1. ∃w2. orderiso w1 w2
[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
[cardleq_setexp] Theorem
⊢ x ≼ x ** e ⇔ x = ∅ ∨ x ≈ 𝟙 ∨ e ≠ ∅
[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_setexp] Theorem
⊢ countable (A ** B) ⇔ B = ∅ ∨ FINITE B ∧ countable A ∨ A ≈ 𝟙 ∨ 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}
[fnOfSet_SING] Theorem
⊢ fnOfSet {(k,v)} = (K NONE)⦇k ↦ SOME v⦈
[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. {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)
[setexp_eq_EMPTY] Theorem
⊢ A ** B = ∅ ⇔ A = ∅ ∧ B ≠ ∅
[tupNONE_IN_BIGPRODi] Theorem
⊢ tup ∈ BIGPRODi Af ⇒ (tup i = NONE ⇔ Af i = NONE)
[wellorder_destWO] Theorem
⊢ wellorder (destWO r)
*)
end
HOL 4, Trindemossen-1