English
Every ordinal a admits a fundamental sequence a.cof.ord f.
Русский
Каждому порядку a существует фундаментальная последовательность, связанная с cof(a).
LaTeX
$$$$\exists f\; \text{IsFundamentalSequence}(a, a.cof.ord, f).$$$$
Lean4
/-- Every ordinal has a fundamental sequence. -/
theorem exists_fundamental_sequence (a : Ordinal.{u}) : ∃ f, IsFundamentalSequence a a.cof.ord f :=
by
suffices h : ∃ o f, IsFundamentalSequence a o f
by
rcases h with ⟨o, f, hf⟩
exact ⟨_, hf.ord_cof⟩
rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
rcases ord_eq ι with ⟨r, wo, hr⟩
let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
let hrr' : r' ↪r r := Subrel.relEmbedding _ _
haveI := hrr'.isWellOrder
refine
⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
· rw [← hι, hr]
· change r (hrr'.1 _) (hrr'.1 _)
rwa [hrr'.2, @enum_lt_enum _ r']
· rw [← hf, lsub_le_iff]
intro i
suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi'
by
rcases h with ⟨i', hi', hfg⟩
exact hfg.trans_lt (lt_blsub _ _ _)
by_cases h : ∀ j, r j i → f j < f i
· refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
rw [bfamilyOfFamily'_typein]
· push_neg at h
obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
· by_contra! H
exact (wo.wf.not_lt_min _ h ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
· rwa [bfamilyOfFamily'_typein]
