lift_le — Mathlib

English

Lifting preserves and reflects the order: a ≤ b iff lift(a) ≤ lift(b).

Русский

Подъём сохраняет и отражает порядок: a ≤ b эквивалентно lift(a) ≤ lift(b).

LaTeX

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

Lean4

@[simp]
theorem lift_le {a b : Ordinal} : lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b :=
  inductionOn₂ a b fun α r _ β s _ => by
    rw [← lift_umax]
    exact lift_type_le.{_, _, u}

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