English
The type-inconstruction assigns to a well-ordered structure the corresponding ordinal type as a principal segment.
Русский
Постановка типа через typein присваивает структурам с заданным порядком соответствующий ординальный тип как главную секцию.
LaTeX
$$$\text{typein}:=(\alpha,r)\mapsto \text{principal segment from }(\alpha,r)\text{ to }(\operatorname{Ordinal})$$$
Lean4
/-- The order type of an element inside a well order.
This is registered as a principal segment embedding into the ordinals, with top `type r`. -/
def typein (r : α → α → Prop) [IsWellOrder α r] : @PrincipalSeg α Ordinal.{u} r (· < ·) :=
by
refine
⟨RelEmbedding.ofMonotone _ fun a b ha ↦ ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r,
fun a ↦ ⟨?_, ?_⟩⟩
· rintro ⟨c, hc⟩
exact trans hc ha
· exact ha
· rintro ⟨b, rfl⟩
exact (PrincipalSeg.ofElement _ _).ordinal_type_lt
· refine inductionOn a ?_
rintro β s wo ⟨g⟩
exact ⟨_, g.subrelIso.ordinal_type_eq⟩
