lift_add — Mathlib

English

The lift operation distributes over ordinal addition: lift(a + b) = lift(a) + lift(b).

Русский

Операция подъема (lift) распределяется над сложением ординалов: lift(a + b) = lift(a) + lift(b).

LaTeX

$$$\mathrm{lift}(a+b) = \mathrm{lift}(a) + \mathrm{lift}(b)\quad (a,b \in \mathrm{Ordinal})$$$

Lean4

@[simp]
theorem lift_add (a b : Ordinal.{v}) : lift.{u} (a + b) = lift.{u} a + lift.{u} b :=
  Quotient.inductionOn₂ a b fun ⟨_α, _r, _⟩ ⟨_β, _s, _⟩ =>
    Quotient.sound
      ⟨(RelIso.preimage Equiv.ulift _).trans
          (RelIso.sumLexCongr (RelIso.preimage Equiv.ulift _) (RelIso.preimage Equiv.ulift _)).symm⟩

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