ind — Mathlib

English

To prove a predicate on X[S^{-1}], it suffices to prove it for all representatives r/s; the result then holds for all q in the localization.

Русский

Чтобы доказать свойство для X[S^{-1}], достаточно доказать его для всех представлений r/s; следовательно, свойство верно для всех q в локализации.

LaTeX

$$∀q, β(q) если ∀r∈X, s∈S, β(r/s)$$

Lean4

@[to_additive (attr := elab_as_elim, cases_eliminator, induction_eliminator)]
protected theorem ind {β : X[S⁻¹] → Prop} (c : ∀ (r : X) (s : S), β (r /ₒ s)) : ∀ q, β q :=
  by
  apply Quotient.ind
  rintro ⟨r, s⟩
  exact c r s

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