typein_ordinal — Mathlib

English

typein on an ordinal equals the lift of that ordinal: typein(o) = lift(o).

Русский

typein ординала равен lift ординала: typein(o) = lift(o).

LaTeX

$$$$ \operatorname{typein}_{<} (o) = \operatorname{lift}(o) $$$$

Lean4

@[simp]
theorem typein_ordinal (o : Ordinal.{u}) : @typein Ordinal (· < ·) _ o = Ordinal.lift.{u + 1} o :=
  by
  refine Quotient.inductionOn o ?_
  rintro ⟨α, r, wo⟩; apply Quotient.sound
  constructor; refine ((RelIso.preimage Equiv.ulift r).trans (enum r).symm).symm

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