enum_typein — Mathlib

English

For any o with o < type r, typein r (enum r ⟨typein r a, typein_lt_type r a⟩) = a.

Русский

Для любого o < type r, 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)\\rangle)) = a$$$

Lean4

@[simp]
theorem enum_typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : enum r ⟨typein r a, typein_lt_type r a⟩ = a :=
  enum_type (PrincipalSeg.ofElement r a)

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