lift_power — Mathlib

English

Lifting commutes with exponentiation: 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_power (a b : Cardinal.{u}) : lift.{v} (a ^ b) = lift.{v} a ^ lift.{v} b :=
  inductionOn₂ a b fun _ _ => mk_congr <| Equiv.ulift.trans (Equiv.ulift.arrowCongr Equiv.ulift).symm

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