mapsTo_smul_closure — Mathlib

English

For any submodule S of a topological R-module M and any scalar c ∈ R, the map x ↦ c•x sends closure(S) into closure(S).

Русский

Для подмодуля S в топологическом R-модуле M и любого скаляра c ∈ R отображение x ↦ c•x отправляет замыкание S в замыкание S.

LaTeX

$$$c\cdot \overline{S} \subseteq \overline{S}$, where $\overline{S}$ denotes the closure of S in M.$$

Lean4

theorem mapsTo_smul_closure (s : Submodule R M) (c : R) : Set.MapsTo (c • ·) (closure s : Set M) (closure s) :=
  have : Set.MapsTo (c • ·) (s : Set M) s := fun _ h ↦ s.smul_mem c h
  this.closure (continuous_const_smul c)

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