isSuccPrelimit_aleph0 — Mathlib

English

aleph0 is a successor-prelimit ordinal: every successor below aleph0 is bounded by a previous one, etc.

Русский

aleph0 является предпределённостью следующего элемента: любое следующее меньше aleph0 ограничено предыдущими.

LaTeX

$$$\text{IsSuccPrelimit}(\aleph_0)$$$

Lean4

theorem isSuccPrelimit_aleph0 : IsSuccPrelimit ℵ₀ :=
  isSuccPrelimit_of_succ_lt fun a ha => by
    rcases lt_aleph0.1 ha with ⟨n, rfl⟩
    rw [← nat_succ]
    apply nat_lt_aleph0

Похожие утверждения