English
For a cardinal c with cof, if ℵ0 ≤ c, then c < c^(cof(ord c)).
Русский
Для кардинала c с cof, если ℵ0 ≤ c, то c < c^(cof(ord c)).
LaTeX
$$$$ \aleph_0 \le c \;\Rightarrow\; c < c^{\operatorname{cof}(\operatorname{ord}(c))}. $$$$
Lean4
theorem lt_power_cof {c : Cardinal.{u}} : ℵ₀ ≤ c → c < c ^ c.ord.cof :=
Cardinal.inductionOn c fun α h => by
rcases ord_eq α with ⟨r, wo, re⟩
have := isSuccLimit_ord h
rw [re] at this ⊢
rcases cof_eq' r this with ⟨S, H, Se⟩
have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_
· simp only [Cardinal.prod_const, Cardinal.lift_id, ← Se, ← mk_sigma, power_def] at this ⊢
refine lt_of_le_of_lt ?_ this
refine ⟨Embedding.ofSurjective ?_ ?_⟩
· exact fun x => x.2.1
·
exact fun a =>
let ⟨b, h, ab⟩ := H a
⟨⟨⟨_, h⟩, _, ab⟩, rfl⟩
· have := typein_lt_type r i
rwa [← re, lt_ord] at this
