isSuccLimit_iff — Mathlib

English

An ordinal is a successor limit exactly when it is nonzero and a succ-prelimit: IsSuccLimit(c) iff (c ≠ 0 ∧ IsSuccPrelimit(c)).

Русский

Кардинал является пределом-последовательностью тогда и только тогда, когда он не равен нулю и является succ-предпределённым: IsSuccLimit(c) ⇔ (c ≠ 0 ∧ IsSuccPrelimit(c)).

LaTeX

$$$\\operatorname{IsSuccLimit}(c) \\iff (c \\neq 0 \\land \\operatorname{IsSuccPrelimit}(c))$$$

Lean4

protected theorem isSuccLimit_iff {c : Cardinal} : IsSuccLimit c ↔ c ≠ 0 ∧ IsSuccPrelimit c :=
  isSuccLimit_iff

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