English
Cof(o) equals the sInf of the set {a : Cardinal | ∃ ι (f : ι → Ordinal), lsub f = o ∧ #ι = a}.
Русский
Cof(o) равен sInf множества {a : Cardinal | ∃ ι (f : ι → Ordinal), lsub f = o ∧ #ι = a}.
LaTeX
$$$ cof(o) = sInf \\{a : Cardinal | \\exists (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a\\}$$$
Lean4
theorem cof_eq_sInf_lsub (o : Ordinal.{u}) :
cof o = sInf {a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a} :=
by
refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
· rintro a ⟨ι, f, hf, rfl⟩
rw [← type_toType o]
refine
(cof_type_le fun a => ?_).trans
(@mk_le_of_injective _ _
(fun s : typein ((· < ·) : o.toType → o.toType → Prop) ⁻¹' Set.range f => Classical.choose s.prop)
fun s t hst => by
let H := congr_arg f hst
rwa [Classical.choose_spec s.prop, Classical.choose_spec t.prop, typein_inj, Subtype.coe_inj] at H)
have := typein_lt_self a
simp_rw [← hf, lt_lsub_iff] at this
obtain ⟨i, hi⟩ := this
refine ⟨enum (α := o.toType) (· < ·) ⟨f i, ?_⟩, ?_, ?_⟩
· rw [type_toType, ← hf]
apply lt_lsub
· rw [mem_preimage, typein_enum]
exact mem_range_self i
· rwa [← typein_le_typein, typein_enum]
· rcases cof_eq (α := o.toType) (· < ·) with ⟨S, hS, hS'⟩
let f : S → Ordinal := fun s => typein LT.lt s.val
refine
⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i) (le_of_forall_lt fun a ha => ?_), by
rwa [type_toType o] at hS'⟩
rw [← type_toType o] at ha
rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
rw [← typein_le_typein, typein_enum] at hb'
exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)
