lift_lift — Mathlib

English

Lifting an ordinal twice is the same as lifting once to the larger universe: lift(lift(a)) = lift_max(a).

Русский

Подъём ординала дважды равен подъёму один раз в более крупную вселенную: lift(lift(a)) = lift(a) на большем уровне.

LaTeX

$$$\\mathrm{lift}(\\mathrm{lift}(a)) = \\mathrm{lift}(\\mathrm{lift\_InitialSeg}.(a)).$$$

Lean4

@[simp]
theorem lift_lift (a : Ordinal.{u}) : lift.{w} (lift.{v} a) = lift.{max v w} a :=
  (liftInitialSeg.trans liftInitialSeg).eq liftInitialSeg a

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