English
span_R (v '' s) = Submodule.map (linearCombination_R v) (supported R R s)
Русский
Замкнутое по образу изображения $v''s$ равно образу линейной комбинации через $v$ от подмодуля, поддерживаемого на $s$.
LaTeX
$$$\operatorname{span}_R(v''s) = \operatorname{map}(\operatorname{linearCombination}_R v)(\operatorname{supported}_R R s)$$$
Lean4
theorem span_image_eq_map_linearCombination (s : Set α) :
span R (v '' s) = Submodule.map (linearCombination R v) (supported R R s) :=
by
apply span_eq_of_le
· intro x hx
rw [Set.mem_image] at hx
apply Exists.elim hx
intro i hi
exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩
· refine map_le_iff_le_comap.2 fun z hz => ?_
have : ∀ i, z i • v i ∈ span R (v '' s) := by
intro c
haveI := Classical.decPred fun x => x ∈ s
by_cases h : c ∈ s
· exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))
· simp [(Finsupp.mem_supported' R _).1 hz _ h]
rw [mem_comap, linearCombination_apply]
refine sum_mem ?_
simp [this]
