Library hydras.Schutte.Countable

A formalization of denumerable sets. by Florian Hatat and Stéphane Desarzens

From Coq Require Import Ensembles Arith ArithRing
     Wellfounded Relations Wf_nat Finite_sets
     Logic.Epsilon Sets.Image Lia.

From ZornsLemma Require Import Classical_Wf CountableTypes Families.

From hydras Require Import MoreEpsilonIota PartialFun GRelations
     Prelude.More_Arith.

Import Nat.

Set Implicit Arguments.

A is countable if there exists an injection from A to Full_set nat.

Section Countable.

  Section Definitions.
    Variable U : Type.
    Variable A : Ensemble U.

Predicate for relations which number the elements of A.

These relations map each element of A to at least one integer, but they are not required to be functional (injectivity is only needed to ensure that A is countable).

Definition rel_numbers (R: GRelation U nat) := rel_injection A Full_set R.

Predicate for relations which enumerate A.

    Definition rel_enumerates (R : GRelation nat U) := rel_surjection Full_set A R.

    Theorem countable_surj :
      Countable A ↔ ∃ R , rel_enumerates R.

  End Definitions.

  Variable U : Type.

  Section Countable_seq_range.

    Definition seq_range (f : nat → U) : Ensemble U :=
      image Full_set f.

    Lemma seq_range_countable :
      ∀ f, Countable (seq_range f).

  End Countable_seq_range.

  Section Countable_bijection.

    Variable V : Type.

    Variable A : Ensemble U.
    Variable B : Ensemble V.
    Variable g : U → V.

    Hypothesis g_bij : fun_bijection A B g.

    Lemma countable_bij_fun :
      Countable A → Countable B.

    Lemma countable_bij_funR :
      Countable B → Countable A.

  End Countable_bijection.

End Countable.

Lemma countable_image : ∀ (U V:Type)(DA : Ensemble U)(f:U →V),
    Countable DA → Countable (image DA f).