lift_mul — Mathlib

English

Lifting preserves multiplication: lift(a*b) = lift(a) * lift(b).

Русский

Поднятие сохраняет умножение: lift(a·b) = lift(a) · lift(b).

LaTeX

$$lift(a*b) = lift(a)*lift(b)$$

Lean4

@[simp]
theorem lift_mul (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.prodLexCongr (RelIso.preimage Equiv.ulift _) (RelIso.preimage Equiv.ulift _)).symm⟩

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