English
Let C be a predicate of three ordinals. If C holds for all triples of order-types arising from well-ordered structures under any well-orders, then C(o1, o2, o3) holds for every triple of ordinals o1, o2, o3.
Русский
Пусть C — предикат к тройке ординалов. Если C выполняется для всех троек типа порядка, полученных из хорошо упорядоченных структур для любых WELL-ORDER, то C(o1, o2, o3) выполняется для любых троек ординалов o1, o2, o3.
LaTeX
$$$\forall C:(\operatorname{Ordinal}\to\operatorname{Ordinal}\to\operatorname{Ordinal}\to\operatorname{Prop}),\ o_1,o_2,o_3:\\operatorname{Ordinal},\\
\left(\forall \alpha,r,[\text{IsWellOrder }\alpha r](\beta,s)[\text{IsWellOrder }\beta s](\gamma,t)[\text{IsWellOrder }\gamma t],\\
C(\operatorname{type} r)(\operatorname{type} s)(\operatorname{type} t)\right)\to C(o_1)(o_2)(o_3).$$
Lean4
/-- `Quotient.inductionOn₃` specialized to ordinals.
Not to be confused with well-founded recursion `Ordinal.induction`. -/
@[elab_as_elim]
theorem inductionOn₃ {C : Ordinal → Ordinal → Ordinal → Prop} (o₁ o₂ o₃ : Ordinal)
(H : ∀ (α r) [IsWellOrder α r] (β s) [IsWellOrder β s] (γ t) [IsWellOrder γ t], C (type r) (type s) (type t)) :
C o₁ o₂ o₃ :=
Quotient.inductionOn₃ o₁ o₂ o₃ fun ⟨α, r, wo₁⟩ ⟨β, s, wo₂⟩ ⟨γ, t, wo₃⟩ => @H α r wo₁ β s wo₂ γ t wo₃
