Library hydras.solutions_exercises.Limit_Infinity

Prove that, for any ordinal 0 < alpha < epsilon0, alpha is a limit if and only if forall ordinal beta < alpha, there exists an infinite number of ordinals betawee beta and alpha

From hydras Require Import Epsilon0 T1.
Open Scope t1_scope.
From Coq Require Import Ensembles Image Compare_dec.

Definition Infinite {A: Type} (E: Ensemble A) :=
  ∃ s: nat → A , injective s ∧ ∀ i, In E (s i).

Section On_alpha.

  Variable alpha : T1.
  Hypothesis Halpha : nf alpha.
  Hypothesis HnonZero : alpha ≠ zero.

  Section S1.
    Hypothesis H : T1limit alpha.

    Variable beta : T1.
    Hypothesis Hbeta : beta t1 < alpha.

    Definition s (i:nat) := beta + S i.

    Lemma L1 (i: nat) : beta t1 < s i t1 < alpha.

Shows that s is infinite

    Lemma L2 : ∀ i, s i t1 < s (S i).

    Lemma L3: injective s.

  End S1.

  Section S2.
    Hypothesis H : ∀ beta, beta t1 < alpha →
                                 ∃ gamma , beta t1 < gamma t1 < alpha.

    Lemma L4 : T1limit alpha.

  End S2.

  Theorem Limit_Infinity : T1limit alpha ↔ (∀ beta,
                                                beta t1 < alpha → Infinite (fun gamma ⇒ beta t1 < gamma t1 < alpha)).

End On_alpha.