induction_on₂ — Mathlib

English

Let p be a predicate on pairs of elements of the localization Local(S). If p holds for all pairs whose components come from representative pairs in M × S (via the canonical embedding mk), then p holds for every pair in Localization(S). In other words, to prove a property of arbitrary localization elements, it suffices to check it on canonical representatives.

Русский

Пусть p — предикат на парах элементов локализации Localization(S). Если p выполняется для всех пар, чьи компоненты получены из представлений в M × S через отображение mk, тогда p выполняется для любых пары в Localization(S). Другими словами, чтобы доказать свойство произвольных элементов локализации, достаточно проверить его на канонических представителях.

LaTeX

$$$\\forall x,y \\in \\mathrm{Localization}(S),\\ \\Big(\\forall u,v \\in M \\times S,\\ p\\big( \\mathrm{mk}(u.1,u.2), \\mathrm{mk}(v.1,v.2)\\big)\\Big) \\Rightarrow p(x,y).$$$

Lean4

@[to_additive (attr := elab_as_elim)]
theorem induction_on₂ {p : Localization S → Localization S → Prop} (x y)
    (H : ∀ x y : M × S, p (mk x.1 x.2) (mk y.1 y.2)) : p x y :=
  induction_on x fun x ↦ induction_on y <| H x

Похожие утверждения