English
The linearCombinationOn construction interprets p : α →₀ R as a linear combination of a subset of the vectors v, landing in the span of v'' s.
Русский
Конструкция linearCombinationOn интерпретирует p : α →₀ R как линейную комбинацию подмножества векторов v, образующую линейное сочетание из их линейного пространства через v'' s.
LaTeX
$$$\\mathrm{linearCombinationOn}(s) : \\mathrm{supported}\\; R\\; R\\; s \\rightarrow_{\\!R} \\mathrm{span}_R (v'' s)$$$
Lean4
/-- `Finsupp.linearCombinationOn M v s` interprets `p : α →₀ R` as a linear combination of a
subset of the vectors in `v`, mapping it to the span of those vectors.
The subset is indicated by a set `s : Set α` of indices.
-/
def linearCombinationOn (s : Set α) : supported R R s →ₗ[R] span R (v '' s) :=
LinearMap.codRestrict _ ((linearCombination _ v).comp (Submodule.subtype (supported R R s))) fun ⟨l, hl⟩ =>
(mem_span_image_iff_linearCombination _).2 ⟨l, hl, rfl⟩
