Background lemmas on ordinals

Auxiliary results about ordinals and recursion on bounded ordinals used in the PCF-theory formalization.

instance Ordinal.instNonemptyElemIioOmega0_leanPool : Nonempty ↑(Set.Iio omega0)

theorem Ordinal.coe_succ_Iio {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} (h : Order.IsSuccPrelimit a) {x : ↑(Set.Iio a)} : ↑(Order.succ x) = Order.succ ↑x

theorem Ordinal.succ_Iio {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} (h : Order.IsSuccPrelimit a) {x : ↑(Set.Iio a)} : Order.succ x = ⟨Order.succ ↑x, ⋯⟩

noncomputable def Ordinal.relIsoNatOmega0 : ℕ ≃o ↑(Set.Iio omega0)

The order isomorphism between ℕ and the first ω ordinals.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ordinal.relIsoNatOmega0_apply (n : ℕ) : relIsoNatOmega0 n = ⟨↑n, ⋯⟩

@[simp]

theorem Ordinal.relIso_nat_omega0_coe_symm_apply (o : ↑(Set.Iio omega0)) : ↑(relIsoNatOmega0.symm o) = ↑o

theorem Ordinal.strictMono_of_succ_lt_omega0 {α : Type u_1} [Preorder α] (f : ↑(Set.Iio omega0) → α) (hf : ∀ (i : ↑(Set.Iio omega0)), f i < f (Order.succ i)) : StrictMono f

theorem Ordinal.lift_sSup {s : Set Ordinal.{u_1}} (hs : BddAbove s) : lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

The lift of a supremum is the supremum of the lifts.

theorem Ordinal.lift_iSup {ι : Type v} {f : ι → Ordinal.{w}} (hf : BddAbove (Set.range f)) : lift.{u, w} (iSup f) = ⨆ (i : ι), lift.{u, w} (f i)

The lift of a supremum is the supremum of the lifts.

def Ordinal.boundedRec {l : Ordinal.{u_2}} {C : ↑(Set.Iio l) → Sort u_1} (H : (o : ↑(Set.Iio l)) → ((o' : ↑(Set.Iio o)) → C ↑o') → C o) (o : ↑(Set.Iio l)) : C o

Strong recursion on Iio l: given a recursor that builds C o from values of C on all predecessors o' : Iio o, we get a function (o : Iio l) → C o.

Equations

• One or more equations did not get rendered due to their size.

theorem Ordinal.boundedRec_eq {l : Ordinal.{u_1}} {C : ↑(Set.Iio l) → Sort u_2} (H : (o : ↑(Set.Iio l)) → ((o' : ↑(Set.Iio o)) → C ↑o') → C o) (o : ↑(Set.Iio l)) : boundedRec H o = H o fun (o' : ↑(Set.Iio o)) => boundedRec H ↑o'

noncomputable def Ordinal.boundedLimitRec' {l : Ordinal.{u_2}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_1} (o : ↑(Set.Iio l)) (zero : motive ⟨0, ⋯⟩) (succAux : (o : ↑(Set.Iio l)) → motive o → motive ⟨↑o + 1, ⋯⟩) (limit : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : motive o

Bounded version of limitRecOn: an Iio l version that mirrors the deprecated boundedLimitRecOn API used in PCF-theory.

Equations

• One or more equations did not get rendered due to their size.

theorem Ordinal.boundedLimitRec'_zero {l : Ordinal.{u_1}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_2} (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨↑o + 1, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : boundedLimitRec' lLim ⟨0, ⋯⟩ H₁ H₂ H₃ = H₁

theorem Ordinal.boundedLimitRec'_succ {l : Ordinal.{u_1}} (lLim : Order.IsSuccLimit l) {motive : ↑(Set.Iio l) → Sort u_2} (o : ↑(Set.Iio l)) (H₁ : motive ⟨0, ⋯⟩) (H₂ : (o : ↑(Set.Iio l)) → motive o → motive ⟨↑o + 1, ⋯⟩) (H₃ : (o : ↑(Set.Iio l)) → Order.IsSuccLimit ↑o → ((o' : ↑(Set.Iio l)) → o' < o → motive o') → motive o) : boundedLimitRec' lLim ⟨↑o + 1, ⋯⟩ H₁ H₂ H₃ = H₂ o (boundedLimitRec' lLim o H₁ H₂ H₃)

theorem Ordinal.not_exists_ssubset_chain_lift {α : Type u} {S : Set α} {ℓ : Ordinal.{v}} (hℓ : Order.IsSuccLimit ℓ) (h : Cardinal.lift.{v, u} (Cardinal.mk ↑S) < Cardinal.lift.{u, v} ℓ.card) : ¬∃ (f : ↑(Set.Iio ℓ) → Set α), (∀ (o : ↑(Set.Iio ℓ)), f o ⊆ S) ∧ ∀ (o p : ↑(Set.Iio ℓ)), o < p → f p ⊂ f o

There doesn't exist a chain of subsets of S of length longer than #S.

theorem Ordinal.mk_Iio_subtype {o : Ordinal.{u_1}} {p : ↑(Set.Iio o)} : Cardinal.mk ↑(Set.Iio p) = Cardinal.mk ↑(Set.Iio ↑p)

theorem Ordinal.two_lt_aleph0 : 2 < Cardinal.aleph0

theorem Ordinal.succ_pred_of_finite {o : Ordinal.{u_1}} (h : 0 < o) (h' : o < omega0) : Order.succ o.pred = o

theorem Ordinal.type_Iio (α : Ordinal.{u}) : (type fun (x1 x2 : ↑(Set.Iio α)) => x1 < x2) = lift.{u + 1, u} α

theorem Ordinal.isSuccLimit_iff' {o : Ordinal.{u_1}} : Order.IsSuccLimit o ↔ o ≠ 0 ∧ ∀ x < o, Order.succ x < o