lift_mul — Mathlib

English

For all cardinals a, b, lift(a·b) = lift(a)·lift(b).

Русский

Для любых кардиналов a, b выполняется lift(a·b) = lift(a)·lift(b).

LaTeX

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

Lean4

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

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