English
Quotient induction on two ordinals specialized to ordinals.
Русский
Квотий-индукция по двум ординалам, адаптированная к ординалам.
LaTeX
$$$\forall C : \mathrm{Ordinal} \to \mathrm{Ordinal} \to \mathrm{Prop}, (o_1 : \mathrm{Ordinal})(o_2 : \mathrm{Ordinal}) (H : \forall (\alpha : Type u_1)(r : \alpha \to \alpha \to \mathrm{Prop}) [IsWellOrder \alpha r] (\beta : Type u_2)(s : \beta \to \beta \to \mathrm{Prop}) [IsWellOrder \beta s], C(\mathrm{type}(r), \mathrm{type}(s))), C(o_1, o_2)$$$
Lean4
/-- `Quotient.inductionOn₂` specialized to ordinals.
Not to be confused with well-founded recursion `Ordinal.induction`. -/
@[elab_as_elim]
theorem inductionOn₂ {C : Ordinal → Ordinal → Prop} (o₁ o₂ : Ordinal)
(H : ∀ (α r) [IsWellOrder α r] (β s) [IsWellOrder β s], C (type r) (type s)) : C o₁ o₂ :=
Quotient.inductionOn₂ o₁ o₂ fun ⟨α, r, wo₁⟩ ⟨β, s, wo₂⟩ => @H α r wo₁ β s wo₂
