English
If a property P holds for all images of morphisms from C under the quotient functor, then P holds for all morphisms in Quotient r between any two quotient objects.
Русский
Если свойство P верно для всех образов морфизмов в Quotient r, полученных через функтор-кватирование, то P верно и для любых морфизмов между любыми двумя объектами в Quotient r.
LaTeX
$$$\forall P:\, \forall a,b:\mathrm{Quotient}(r),\; (\forall x,y\in C,\; f:\, x\to y,\; P((\mathrm{functor}\ r).map f))\; \Rightarrow\; \forall f:\, a\to b,\; P(f).$$$
Lean4
protected theorem induction {P : ∀ {a b : Quotient r}, (a ⟶ b) → Prop}
(h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)) : ∀ {a b : Quotient r} (f : a ⟶ b), P f :=
by
rintro ⟨x⟩ ⟨y⟩ ⟨f⟩
exact h f
