smul_closure_subset — Mathlib

English

For any S, the inclusion c•closure(S) ⊆ closure(S) holds, i.e., closure(S) is stable under scalar multiplication.

Русский

Для любого S выполняется включение c•closure(S) ⊆ closure(S); замыкание стабильно относительно умножения на скаляр.

LaTeX

$$$c\cdot \overline{S} \subseteq \overline{S}$.$$

Lean4

theorem smul_closure_subset (s : Submodule R M) (c : R) : c • closure (s : Set M) ⊆ closure (s : Set M) :=
  (s.mapsTo_smul_closure c).image_subset

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