English
To prove a statement about ordinals, it suffices to prove it for the order types of well-ordered sets.
Русский
Чтобы доказать утверждение для ординалов, достаточно доказать его для типов порядков всех хорошо упорядоченных множеств.
LaTeX
$$$\forall C:\operatorname{Ordinal}\to\operatorname{Prop},\ o:\operatorname{Ordinal},\left(\forall \alpha\ [\text{LinearOrder }\alpha] [\text{WellFoundedLT }\alpha],\; C(\operatorname{typeLT}\alpha)\right)\Rightarrow C(o).$$
Lean4
/-- To prove a result on ordinals, it suffices to prove it for order types of well-orders. -/
@[elab_as_elim]
theorem inductionOnWellOrder {C : Ordinal → Prop} (o : Ordinal)
(H : ∀ (α) [LinearOrder α] [WellFoundedLT α], C (typeLT α)) : C o :=
inductionOn o fun α r wo ↦ @H α (linearOrderOfSTO r) wo.toIsWellFounded
