lift_preOmega — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem _root_.Ordinal.lift_preOmega (o : Ordinal.{u}) :
    Ordinal.lift.{v} (preOmega o) = preOmega (Ordinal.lift.{v} o) := by
  rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]

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