English
Let p be a predicate on triple elements of Localization(S). If p holds for all triples coming from triples in M × S (via mk), then p holds for every triple in Localization(S). This extends the two-variable induction to three variables.
Русский
Пусть p — предикат на тройках элементов Localization(S). Если p верно для всех троек, полученных из троек в M × S через mk, тогда p верно и для любых троек в Localization(S).
LaTeX
$$$\\forall x,y,z \\in \\mathrm{Localization}(S),\\ (\\forall a,b,c \\in M \\times S,\\ p(\\mathrm{mk}(a.1,a.2),\\mathrm{mk}(b.1,b.2),\\mathrm{mk}(c.1,c.2))) \\Rightarrow p(x,y,z).$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem induction_on₃ {p : Localization S → Localization S → Localization S → Prop} (x y z)
(H : ∀ x y z : M × S, p (mk x.1 x.2) (mk y.1 y.2) (mk z.1 z.2)) : p x y z :=
induction_on₂ x y fun x y ↦ induction_on z <| H x y
