Theory Countable
section ‹Countable Sets›
theory Countable
imports Nats Axiom_Of_Choice Nat_Parity Cardinality
begin
text ‹The definition below corresponds to Definition 2.6.9 in Halvorson.›
definition epi_countable :: "cset ⇒ bool" where
"epi_countable X ⟷ (∃ f. f : ℕ⇩c → X ∧ epimorphism f)"
lemma emptyset_is_not_epi_countable:
"¬ epi_countable ∅"
using comp_type emptyset_is_empty epi_countable_def zero_type by blast
text ‹The fact that the empty set is not countable according to the definition from Halvorson
(@{thm epi_countable_def}) motivated the following definition.›
definition countable :: "cset ⇒ bool" where
"countable X ⟷ (∃ f. f : X → ℕ⇩c ∧ monomorphism f)"
lemma epi_countable_is_countable:
assumes "epi_countable X"
shows "countable X"
using assms countable_def epi_countable_def epis_give_monos by blast
lemma emptyset_is_countable:
"countable ∅"
using countable_def empty_subset subobject_of_def2 by blast
lemma natural_numbers_are_countably_infinite:
"countable ℕ⇩c ∧ is_infinite ℕ⇩c"
by (meson CollectI Peano's_Axioms countable_def injective_imp_monomorphism is_infinite_def successor_type)
lemma iso_to_N_is_countably_infinite:
assumes "X ≅ ℕ⇩c"
shows "countable X ∧ is_infinite X"
by (meson assms countable_def is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic isomorphic_is_symmetric larger_than_infinite_is_infinite natural_numbers_are_countably_infinite)
lemma smaller_than_countable_is_countable:
assumes "X ≤⇩c Y" "countable Y"
shows "countable X"
by (smt assms cfunc_type_def comp_type composition_of_monic_pair_is_monic countable_def is_smaller_than_def)
lemma iso_pres_countable:
assumes "X ≅ Y" "countable Y"
shows "countable X"
using assms is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic smaller_than_countable_is_countable by blast
lemma NuN_is_countable:
"countable(ℕ⇩c ∐ ℕ⇩c)"
using countable_def epis_give_monos halve_with_parity_iso halve_with_parity_type iso_imp_epi_and_monic by smt
text ‹The lemma below corresponds to Exercise 2.6.11 in Halvorson.›
lemma coproduct_of_countables_is_countable:
assumes "countable X" "countable Y"
shows "countable(X ∐ Y)"
unfolding countable_def
proof-
obtain x where x_def: "x : X → ℕ⇩c ∧ monomorphism x"
using assms(1) countable_def by blast
obtain y where y_def: "y : Y → ℕ⇩c ∧ monomorphism y"
using assms(2) countable_def by blast
obtain n where n_def: " n : ℕ⇩c ∐ ℕ⇩c → ℕ⇩c ∧ monomorphism n"
using NuN_is_countable countable_def by blast
have xy_type: "x ⨝⇩f y : X ∐ Y → ℕ⇩c ∐ ℕ⇩c"
using x_def y_def by (typecheck_cfuncs, auto)
then have nxy_type: "n ∘⇩c (x ⨝⇩f y) : X ∐ Y → ℕ⇩c"
using comp_type n_def by blast
have "injective(x ⨝⇩f y)"
using cfunc_bowtieprod_inj monomorphism_imp_injective x_def y_def by blast
then have "monomorphism(x ⨝⇩f y)"
using injective_imp_monomorphism by auto
then have "monomorphism(n ∘⇩c (x ⨝⇩f y))"
using cfunc_type_def composition_of_monic_pair_is_monic n_def xy_type by auto
then show "∃f. f : X ∐ Y → ℕ⇩c ∧ monomorphism f"
using nxy_type by blast
qed
end