English
A version of induction on Quotients for predicates of two arguments: if for all x∈M,y∈N, C(x,y) then C(p,q) for p,q in c.Quotient and d.Quotient respectively.
Русский
Версия индукции на двух факторных частях: если для всех x∈M,y∈N выполняется C(x,y), то C(p,q) для p∈c.Quotient, q∈d.Quotient.
LaTeX
$$$\\forall p:\\; c.Quotient,\\forall q:\\; d.Quotient,\\; (\\forall x:\\; M,y:\\; N,\\; C(x,y))\\Rightarrow C(p,q)$$$
Lean4
/-- A version of `Con.induction_on` for predicates which takes two arguments. -/
@[to_additive (attr := elab_as_elim) /-- A version of `AddCon.induction_on` for predicates which takes two arguments. -/
]
protected theorem induction_on₂ {d : Con N} {C : c.Quotient → d.Quotient → Prop} (p : c.Quotient) (q : d.Quotient)
(H : ∀ (x : M) (y : N), C x y) : C p q :=
Quotient.inductionOn₂' p q H
