English
Reiterates the equivalence between aleph-null compared to cof and IsSuccLimit.
Русский
Повторение эквивалентности между aleph-null и cof и IsSuccLimit.
LaTeX
$$$$\aleph_0 \le cof(o) \iff IsSuccLimit(o). $$$$
Lean4
theorem aleph0_le_cof {o} : ℵ₀ ≤ cof o ↔ IsSuccLimit o :=
by
rcases zero_or_succ_or_isSuccLimit o with (rfl | ⟨o, rfl⟩ | l)
· simp [Cardinal.aleph0_ne_zero]
· simp [Cardinal.one_lt_aleph0]
· simp only [l, iff_true]
refine le_of_not_gt fun h => ?_
obtain ⟨n, e⟩ := Cardinal.lt_aleph0.1 h
have := cof_cof o
rw [e, ord_nat] at this
cases n
· apply l.ne_bot
simpa using e
· rw [natCast_succ, cof_succ] at this
rw [← this, cof_eq_one_iff_is_succ] at e
rcases e with ⟨a, rfl⟩
exact not_isSuccLimit_succ _ l
