lift_lift — Mathlib

English

Lifting a cardinal sequentially through v and then w equals lifting directly to max(v,w).

Русский

Подача кардинала последовательно через v и затем через w равна подъему напрямую до max(v,w).

LaTeX

$$$\\mathrm{lift}^{w}( \\mathrm{lift}^{v} a) = \\mathrm{lift}^{\\max\\,v\\,w} a$$$

Lean4

@[simp]
theorem lift_lift.{u_1} (a : Cardinal.{u_1}) : lift.{w} (lift.{v} a) = lift.{max v w} a :=
  inductionOn a fun _ => (Equiv.ulift.trans <| Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

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