ord_inj

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.ord_inj

English

ord is injective: ord(a) = ord(b) iff a = b.

Русский

ord(а) = ord(б) если и только если a = b.

LaTeX

$$$ \operatorname{ord}(a) = \operatorname{ord}(b) \iff a = b $$$

Lean4

@[simp]
theorem ord_inj {a b : Cardinal} : a.ord = b.ord ↔ a = b :=
  ord_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru