span_le_supported_biUnion_support

English

The span of a set of finsupp maps is contained in the supported submodule on the union of their supports.

Русский

Линейное замыкание множества функций с конечной опорой вложено в подмодуль поддержки на объединении их опор.

LaTeX

$$$\operatorname{span}_R(s) \le \mathrm{supported}(M,R,\bigcup_{x\in s} x.{\text{support}})$$$

Lean4

theorem span_le_supported_biUnion_support (s : Set (α →₀ M)) : span R s ≤ supported M R (⋃ x ∈ s, x.support) :=
  span_le.mpr fun _ h ↦ subset_biUnion_of_mem h (u := (·.support.toSet))

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