locally_of — Mathlib

English

If a property P respects isomorphisms and f satisfies P, then f is Locally P.

Русский

Если свойство P сохраняет изоморфизмы и f удовлетворяет P, то f локально удовлетворяет P.

LaTeX

$$$\text{If }P\text{ respects iso and }P(f),\text{ then }\text{Locally }P(f).$$$

Lean4

/-- If `f` satisfies `P`, then in particular it satisfies `Locally P`. -/
theorem locally_of (hP : RespectsIso P) (f : R →+* S) (hf : P f) : Locally P f :=
  by
  use { 1 }
  let e : S ≃+* Localization.Away (1 : S) := (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).toRingEquiv
  simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
  exact hP.left f e hf

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