English
Two-variable induction principle for Quotients: if p holds for mk'' a₁ and mk'' a₂ for all a₁,a₂, then p holds for q₁,q₂.
Русский
Двухпеременная индукция по квантинам: если p верно для mk'' a₁ и mk'' a₂ для всех a₁,a₂, тогда p верно для q₁,q₂.
LaTeX
$$$(\\forall a_1:\\, \\alpha)(\\forall a_2:\\, \\beta), p(\\mathrm{mk}'' a_1)(\\mathrm{mk}'' a_2) \\Rightarrow p(q_1)(q_2)$$$
Lean4
/-- A version of `Quotient.ind₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
instead of instance arguments. -/
@[elab_as_elim]
protected theorem ind₂' {p : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a₁ a₂, p (Quotient.mk'' a₁) (Quotient.mk'' a₂))
(q₁ : Quotient s₁) (q₂ : Quotient s₂) : p q₁ q₂ :=
Quotient.ind₂ h q₁ q₂
