English
There is a canonical way to define a value on ordinals by specifying a value on order types of well-orders, together with a coherence condition ensuring consistency across order-type isomorphisms.
Русский
Существует канонический способ задать значение на ординалах через задание значений на типах порядков хорошо упорядоченных множеств и согласование по эквивалентности порядка.
LaTeX
$$$\mathrm{liftOnWellOrder} : (o: \operatorname{Ordinal}) \to (\forall (\alpha) [\text{LinearOrder }\alpha] [\text{WellFoundedLT }\alpha], \delta) \to \,\delta,$
"liftOnWellOrder" assigns to each ordinal a value in a fixed δ, depending on a family f with a coherence condition c that identifies values for order-type-equivalent well-orders.$$
Lean4
/-- To define a function on ordinals, it suffices to define them on order types of well-orders.
Since `LinearOrder` is data-carrying, `liftOnWellOrder_type` is not a definitional equality, unlike
`Quotient.liftOn_mk` which is always def-eq. -/
def liftOnWellOrder {δ : Sort v} (o : Ordinal) (f : ∀ (α) [LinearOrder α] [WellFoundedLT α], δ)
(c :
∀ (α) [LinearOrder α] [WellFoundedLT α] (β) [LinearOrder β] [WellFoundedLT β], typeLT α = typeLT β → f α = f β) :
δ :=
Quotient.liftOn o (fun w ↦ @f w.α (linearOrderOfSTO w.r) w.wo.toIsWellFounded) fun w₁ w₂ h ↦
@c w₁.α (linearOrderOfSTO w₁.r) w₁.wo.toIsWellFounded w₂.α (linearOrderOfSTO w₂.r) w₂.wo.toIsWellFounded
(Quotient.sound h)
