le_enumOrd_self — Mathlib

English

If s is not bounded above, then every ordinal a satisfies a ≤ enumOrd(s, a).

Русский

Если s не ограничено сверху, то для каждого ординала a выполняется a ≤ enumOrd(s, a).

LaTeX

$$$\forall s : \mathrm{Set}\ \mathrm{Ordinal},\, \neg \mathrm{BddAbove}(s) \Rightarrow \forall a : \mathrm{Ordinal},\, a \le \mathrm{enumOrd}(s,a)$$$

Lean4

theorem le_enumOrd_self (hs : ¬BddAbove s) {a} : a ≤ enumOrd s a :=
  (enumOrd_strictMono hs).le_apply

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