English
Let δ be a predicate on pairs of quotients δ : Quot r → Quot s → Prop. If q1 : Quot r and q2 : Quot s are given, and δ holds for every pair of representatives, i.e. ∀ a : α, ∀ b : β, δ (Quot.mk r a) (Quot.mk s b), then δ q1 q2 holds. In other words, proving a property for all representatives suffices to establish it for arbitrary quotients.
Русский
Пусть δ — отношение на пары классов эквивалентности δ : Quot r → Quot s → Prop. Если даны q1 : Quot r и q2 : Quot s и δ выполняется для всех пар представителей, то δ q1 q2 выполняется. Иными словами, достаточно доказать свойство для всех представителей, чтобы установить его для любых квот.
LaTeX
$$$\\forall q_1: \\mathrm{Quot}(r),\\, \\forall q_2: \\mathrm{Quot}(s),\\,\\Big(\\forall a:\\alpha,\\forall b:\\beta,\\ \\delta(\\overline{a},\\overline{b})\\Big)\\Rightarrow \\delta(q_1,q_2) $$$
Lean4
@[elab_as_elim]
protected theorem induction_on₂ {δ : Quot r → Quot s → Prop} (q₁ : Quot r) (q₂ : Quot s)
(h : ∀ a b, δ (Quot.mk r a) (Quot.mk s b)) : δ q₁ q₂ :=
Quot.ind (β := fun a ↦ δ a q₂) (fun a₁ ↦ Quot.ind (fun a₂ ↦ h a₁ a₂) q₂) q₁
