id_le_enumOrd — Mathlib

English

If s is not bounded above, then the identity function is less than or equal to the enumeration function: id ≤ enumOrd(s).

Русский

Если s не ограничено сверху, то тождественная функция меньше или равна функции enumOrd(s).

LaTeX

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

Lean4

theorem id_le_enumOrd (hs : ¬BddAbove s) : id ≤ enumOrd s :=
  (enumOrd_strictMono hs).id_le

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