span_eq_range_linearCombination — Mathlib

English

For any set s ⊆ M, span_R s = range (linearCombination_R Subtype.val).

Русский

Для подмножества $s$ множества $M$ выполняется равенство: замкнутое по $s$ подмодуль равно образу линейной комбинации по инклудии.

LaTeX

$$$\operatorname{span}_R(s) = \operatorname{range}(\operatorname{linearCombination}_R (\operatorname{Subtype.val})).$$$

Lean4

/-- A version of `Finsupp.range_linearCombination` which is useful for going in the other
direction -/
theorem span_eq_range_linearCombination (s : Set M) : span R s = LinearMap.range (linearCombination R ((↑) : s → M)) :=
  by rw [range_linearCombination, Subtype.range_coe_subtype, Set.setOf_mem_eq]

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