ind — Mathlib

English

Induction principle: if p holds for all mk y, then p holds for all localization elements.

Русский

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

LaTeX

$$$ \forall x:\text{Localization}(S),\ p(x) $$$

Lean4

@[to_additive (attr := elab_as_elim, induction_eliminator, cases_eliminator)]
theorem ind {p : Localization S → Prop} (H : ∀ y : M × S, p (mk y.1 y.2)) (x) : p x :=
  rec (fun a b ↦ H (a, b)) (fun _ ↦ rfl) x

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