induction_on — Mathlib

English

Induction principle variant: if p holds for every mk, then p holds for every localization element.

Русский

Вариант принципа индукции: если p верно для каждого mk, то верно и для каждого элемента локализации.

LaTeX

$$$ induction\_on(x)\ H : \forall y, p(\mathrm{mk}(y)) \Rightarrow p(x) $$$

Lean4

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

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