lift_ord — Mathlib

English

lifting commutes with ord: lift(ord c) = ord(lift c).

Русский

взятие порядка и переход вверх по типу коммутируются: lift(ord(c)) = ord(lift(c)).

LaTeX

$$$ \operatorname{lift}(\operatorname{ord}(c)) = \operatorname{ord}(\operatorname{lift}(c)) $$$

Lean4

@[simp]
theorem lift_ord (c) : Ordinal.lift.{u, v} (ord c) = ord (lift.{u, v} c) :=
  by
  refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_
  · rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
  · rw [ord_le, ← lift_card, card_ord]

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