isSuccLimit — Mathlib

English

If c is a strong limit cardinal, then c is a successor limit.

Русский

Если c — сильный предел кардинал, то он является пределом-суперчислом (succ-limit).

LaTeX

$$$\\forall c\\ (H : IsStrongLimit\\, c)\\,\\, IsSuccLimit\\, c$$$

Lean4

protected theorem isSuccLimit {c} (H : IsStrongLimit c) : IsSuccLimit c :=
  by
  rw [Cardinal.isSuccLimit_iff]
  exact ⟨H.ne_zero, isSuccPrelimit_of_succ_lt fun x h ↦ (succ_le_of_lt <| cantor x).trans_lt (H.two_power_lt h)⟩

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