enumOrd_inj — Mathlib

English

For not bounded above s, enumOrd s is injective and: enumOrd s a = enumOrd s b iff a = b.

Русский

Для неограниченного сверху множества s, enumOrd s инъективен и: enumOrd s a = enumOrd s b ⇔ a = b.

LaTeX

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

Lean4

theorem enumOrd_inj (hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a = enumOrd s b ↔ a = b :=
  (enumOrd_injective hs).eq_iff

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