eq_top_of_isLocalized'_span — Mathlib

English

If N localized at every P is the whole module, then N is the whole module.

Русский

Если локализация N по каждому P даёт весь модуль, то сам N равен всему модулю.

LaTeX

$$$$\forall P\,[P^{\mathrm{Max}}],\; N localized^{P} = MTop \Rightarrow N = MTop.$$$$

Lean4

theorem eq_top_of_isLocalized'_span {N : Submodule R M} (h : ∀ r : s, N.localized' (Rₚ r) (.powers r.1) (f r) = ⊤) :
    N = ⊤ :=
  eq_of_isLocalized'_span s span_eq Rₚ Mₚ f fun _ ↦ by simp only [h, Submodule.localized'_top]

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