lift_lt

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.lift_lt

English

Lifting preserves strict order: lift(a) < lift(b) iff a < b.

Русский

Подъём сохраняет строгий порядок: lift(a) < lift(b) тогда и только тогда, когда a < b.

LaTeX

$$$\\forall a,b:\\, \\text{lift}(a) < \\text{lift}(b) \\iff a < b.$$$

Lean4

@[simp]
theorem lift_lt {a b : Ordinal} : lift.{u, v} a < lift.{u, v} b ↔ a < b := by simp_rw [lt_iff_le_not_ge, lift_le]

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

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

Разделы

Аффилиация

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