lsub_typein — Mathlib

English

For an ordinal o, lsub of the type embedding typein corresponding to o recovers o.

Русский

Для ординала o равенство lsub(typein) = o, т.е. восстанавливается o через встраивание типа.

LaTeX

$$$\operatorname{lsub}(\text{typein} ) = o$$$

Lean4

@[simp]
theorem lsub_typein (o : Ordinal) : lsub.{u, u} (typein (α := o.toType) (· < ·)) = o :=
  (lsub_le.{u, u} typein_lt_self).antisymm
    (by
      by_contra! h
      have h := h.trans_eq (type_toType o).symm
      simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) ⟨_, h⟩))

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