English
A version of induction on quotients for three implicit setoid arguments.
Русский
Версия индукции по кватам для трёх неявных аргументов множества эквивалентности.
LaTeX
$$$(\\forall q_1:\\, \\operatorname{Quotient}(s_1))(\\forall q_2:\\, \\operatorname{Quotient}(s_2))(\\forall q_3:\\, \\operatorname{Quotient}(s_3), p q_1 q_2 q_3)$$$
Lean4
/-- A version of `Quotient.inductionOn₃` taking `{s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}`
as implicit arguments instead of instance arguments. -/
@[elab_as_elim]
protected theorem inductionOn₃' {p : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁)
(q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a₁ a₂ a₃, p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)) :
p q₁ q₂ q₃ :=
Quotient.inductionOn₃ q₁ q₂ q₃ h
