Structure cardinalTheory


Source File Identifier index Theory binding index

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


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1