limit_lt — Mathlib

English

Let f be a normal function on ordinals. If o is a successor-limit ordinal, then for every ordinal a, a < f(o) if and only if there exists b < o with a < f(b).

Русский

Пусть f — нормальная функция на ординалах. Пусть o является succ-пределом. Тогда для любого a выполняется: a < f(o) тогда и только тогда, существует b < o such that a < f(b).

LaTeX

$$$\forall f\,\bigl(\mathrm{IsNormal}(f)\bigr)\,\forall o\,\mathrm{IsSuccLimit}(o)\;\forall a,\; a < f(o) \iff \exists b < o\; (a < f(b)).$$$

Lean4

theorem limit_lt {f} (H : IsNormal f) {o} (h : IsSuccLimit o) {a} : a < f o ↔ ∃ b < o, a < f b :=
  H.lt_iff_exists_lt h

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