ord_le_ord

Mathlib.SetTheory.Ordinal.Basic

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

English

For cardinals c1, c2, ord(c1) ≤ ord(c2) if and only if c1 ≤ c2.

Русский

Для кардиналов c1, c2 имеет место: ord(c1) ≤ ord(c2) тогда и только тогда, когда c1 ≤ c2.

LaTeX

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

Lean4

@[simp]
theorem ord_le_ord {c₁ c₂} : ord c₁ ≤ ord c₂ ↔ c₁ ≤ c₂ :=
  gciOrdCard.l_le_l_iff

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

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

Разделы

Аффилиация

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