ord_lt_ord

Mathlib.SetTheory.Ordinal.Basic

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

English

For cardinals c1, c2, ord(c1) < ord(c2) iff c1 < c2.

Русский

Для кардиналов c1, c2: ord(c1) < ord(c2) эквивалентно c1 < c2.

LaTeX

$$$ \operatorname{ord}(c_1) < \operatorname{ord}(c_2) \iff c_1 < c_2 $$$

Lean4

@[simp]
theorem ord_lt_ord {c₁ c₂} : ord c₁ < ord c₂ ↔ c₁ < c₂ :=
  ord_strictMono.lt_iff_lt

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

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

Разделы

Аффилиация

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