English
Let δ be a predicate on triples of quotients δ : Quot r → Quot s → Quot t → Prop. If q1 : Quot r, q2 : Quot s, q3 : Quot t and δ holds for all triples of representatives, i.e. ∀ a : α, ∀ b : β, ∀ c : γ, δ (Quot.mk r a) (Quot.mk s b) (Quot.mk t c), then δ q1 q2 q3.
Русский
Пусть δ — предикат на тройках квот δ : Quot r → Quot s → Quot t → Prop. Если даны q1 : Quot r, q2 : Quot s, q3 : Quot t и δ выполняется для всех троек представителей, т.е. ∀ a, b, c, δ (Quot.mk r a) (Quot.mk s b) (Quot.mk t c), тогда δ q1 q2 q3.
LaTeX
$$$\\forall q_1: \\mathrm{Quot}(r),\\, \\forall q_2: \\mathrm{Quot}(s),\\, \\forall q_3: \\mathrm{Quot}(t),\\,\\Big(\\forall a:\\alpha,\\forall b:\\beta,\\forall c:\\gamma,\\ \\delta(\\overline{a},\\overline{b},\\overline{c})\\Big)\\Rightarrow \\delta(q_1,q_2,q_3) $$$
Lean4
@[elab_as_elim]
protected theorem induction_on₃ {δ : Quot r → Quot s → Quot t → Prop} (q₁ : Quot r) (q₂ : Quot s) (q₃ : Quot t)
(h : ∀ a b c, δ (Quot.mk r a) (Quot.mk s b) (Quot.mk t c)) : δ q₁ q₂ q₃ :=
Quot.ind (β := fun a ↦ δ a q₂ q₃)
(fun a₁ ↦ Quot.ind (β := fun b ↦ δ _ b q₃) (fun a₂ ↦ Quot.ind (fun a₃ ↦ h a₁ a₂ a₃) q₃) q₂) q₁
