forall_lt — Mathlib

English

If o is an accumulation point of S, then o is a successor-limit ordinal (i.e., not a zero, and not a pure successor).

Русский

Если o является точкой накопления множества S, то o является предельным предшественником (не ноль и не простой следующий за чем-либо).

LaTeX

$$IsSuccLimit(o) is implied by IsAcc(S).$$

Lean4

theorem forall_lt {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : ∀ p < o, (S ∩ Ioo p o).Nonempty :=
  ((isAcc_iff _ _).mp h).2

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