Structure countable_typesTheory

signature countable_typesTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val countable_split : thm
    val list_countable : thm
    val unit_countable : thm
(*
   [hol] Parent theory of "countable_types"
   
   [countable_split]  Theorem
      
      ⊢ ∀X f m.
          INJ f X 𝕌(:num list # α list) ∧
          (∀x y. x ∈ X ∧ MEM y (SND (f x)) ⇒ y ∈ X ∧ m y < m x) ⇒
          countable X
   
   [list_countable]  Theorem
      
      ⊢ countable Lset ⇔ countable (BIGUNION (IMAGE set Lset))
   
   [unit_countable]  Theorem
      
      ⊢ countable 𝕌(:unit)
   
   
*)
end

HOL 4, Trindemossen-2