English
A two-argument induction principle on Subobject X: if a property P holds for all morphisms into X, then it holds for any pair of subobjects.
Русский
Двухаргументная индукция на Subobject X: если свойство P верно для всех морфизмов в X, тогда оно верно для любой пары подобъектов.
LaTeX
$$$\\text{ind}_2: \\forall p, (\\forall f,g: A,B \\to X) [Mono f] [Mono g], p(\\mathrm{Subobject.mk} f)(\\mathrm{Subobject.mk} g) \\Rightarrow \\forall P Q, p P Q$$$
Lean4
protected theorem ind₂ {X : C} (p : Subobject X → Subobject X → Prop)
(h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [Mono f] [Mono g], p (Subobject.mk f) (Subobject.mk g))
(P Q : Subobject X) : p P Q := by
apply Quotient.inductionOn₂'
intro a b
exact h a.arrow b.arrow
