localized₀_top — Mathlib

English

Localization of bottom to localized' equals bottom; i.e., the bottom element maps to bottom in the localized submodule.

Русский

Локализация нижнего элемента в localized' равна нижнему элементу.

LaTeX

$$$\\operatorname{localized}'(S,p,f)\\,\\bot = \\bot.$$$

Lean4

@[simp]
theorem localized₀_top : (⊤ : Submodule R M).localized₀ p f = ⊤ :=
  by
  rw [← top_le_iff]
  rintro x _
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
  exact ⟨x, trivial, s, rfl⟩

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