lift_preAleph — Mathlib

English

For every ordinal o, lift(preAleph(o)) = preAleph(lift(o)).

Русский

Пусть o — ординал. Тогда lifting(preAleph(o)) = preAleph(lift(o)).

LaTeX

$$$$ \forall o:\mathrm{Ordinal}, \operatorname{lift}(\operatorname{preAleph}(o)) = \operatorname{preAleph}(\operatorname{lift}(o)). $$$$

Lean4

@[simp]
theorem lift_preAleph (o : Ordinal.{u}) : lift.{v} (preAleph o) = preAleph (Ordinal.lift.{v} o) :=
  (preAleph.toInitialSeg.trans liftInitialSeg).eq (Ordinal.liftInitialSeg.trans preAleph.toInitialSeg) o

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