English
The induction principle for propositions on elements of a quotient by a congruence: if C holds on all representatives x ∈ M, then C holds on any q ∈ c.Quotient.
Русский
Индуктивный принцип для предикатов над элементами фактор-множества по конгруэнции: если C верно для всех представителиныx ∈ M, то C верно для любого q ∈ c.Quotient.
LaTeX
$$$\\forall q:\\; c.Quotient,\\; (\\forall x:\\; M,\\; C(Con.toQuotient x))\\Rightarrow C(q)$$$
Lean4
/-- The inductive principle used to prove propositions about the elements of a quotient by a
congruence relation. -/
@[to_additive (attr := elab_as_elim) /-- The inductive principle used to prove propositions about
the elements of a quotient by an additive congruence relation. -/
]
protected theorem induction_on {C : c.Quotient → Prop} (q : c.Quotient) (H : ∀ x : M, C x) : C q :=
Quotient.inductionOn' q H
