enumOrd_le_of_forall_lt — Mathlib

English

For any s with Not (BddAbove s), the range of enumOrd(s) is exactly s: range (enumOrd s) = s.

Русский

Для любого s, не ограниченного сверху, множество значений enumOrd(s) совпадает с s: range (enumOrd s) = s.

LaTeX

$$$$ \\text{range}(\\mathrm{enumOrd}(s)) = s \\\\ \\text{(при } \\neg BddAbove(s) \\text{)} $$$$

Lean4

theorem enumOrd_le_of_forall_lt (ha : a ∈ s) (H : ∀ b < o, enumOrd s b < a) : enumOrd s o ≤ a :=
  by
  rw [enumOrd]
  exact csInf_le' ⟨ha, H⟩

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