lift_add — Mathlib

English

Lift distributes over addition: lift(a + b) = lift(a) + lift(b).

Русский

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

LaTeX

$$$\operatorname{lift}(a + b) = \operatorname{lift}(a) + \operatorname{lift}(b)$$$

Lean4

@[simp]
theorem lift_add (a b : Cardinal.{u}) : lift.{v} (a + b) = lift.{v} a + lift.{v} b :=
  inductionOn₂ a b fun _ _ => mk_congr <| Equiv.ulift.trans (Equiv.sumCongr Equiv.ulift Equiv.ulift).symm

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