enumOrd_le_enumOrd — Mathlib

English

For not bounded above s, enumOrd s is order-preserving: enumOrd s a ≤ enumOrd s b iff a ≤ b.

Русский

Для неограниченного сверху s, enumOrd s сохраняет порядок: enumOrd s a ≤ enumOrd s b iff a ≤ b.

LaTeX

$$$\forall s,\ Not (BddAbove s)\Rightarrow\forall a,b,\ enumOrd s a \le\ enumOrd s b \iff a \le b$$$

Lean4

theorem enumOrd_le_enumOrd (hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a ≤ enumOrd s b ↔ a ≤ b :=
  (enumOrd_strictMono hs).le_iff_le

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