English
A version of quotient induction: if p holds for mk'' a for all a, then p holds for every q in Quotient s₁.
Русский
Версия индукции по частям отношения эквивалентности: если p верно для mk'' a для всех a, то p верно и для каждого q в Quotient s₁.
LaTeX
$$$(\\forall a:\\, \\alpha, p(\\mathrm{mk}'' a)) \\Rightarrow \\forall q:\\, \\operatorname{Quotient}(s_1), p(q)$$$
Lean4
/-- A version of `Quotient.ind` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument. -/
@[elab_as_elim]
protected theorem ind' {p : Quotient s₁ → Prop} (h : ∀ a, p (Quotient.mk'' a)) (q : Quotient s₁) : p q :=
Quotient.ind h q
