closure_subset_span — Mathlib

English

The closure of a set under addition and scalar multiplication sits inside the span of the set.

Русский

Замыкание множества по сложению и умножению на скаляр лежит в span.

LaTeX

$$$ AddSubmonoid.closure s \subseteq (\operatorname{span} R s).toAddSubmonoid. $$$

Lean4

theorem closure_subset_span {s : Set M} : (AddSubmonoid.closure s : Set M) ⊆ span R s :=
  (@AddSubmonoid.closure_le _ _ _ (span R s).toAddSubmonoid).mpr subset_span

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