enum_type — Mathlib

English

For any a in α, typein r (enum r ⟨typein r a, typein_lt_type r a⟩) = a.

Русский

Пусть a ∈ α; тогда typein r (enum r ⟨typein r a, typein_lt_type r a⟩) = a.

LaTeX

$$$typein_r(\\mathrm{enum}_r(⟨\\mathrm{typein}_r(a), \\mathrm{typein\_lt\_type}_r(a)⟩)) = a$$$

Lean4

theorem enum_type {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] (f : s ≺i r)
    {h : type s < type r} : enum r ⟨type s, h⟩ = f.top :=
  (typein r).injective <| (typein_enum _ _).trans (typein_top _).symm

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