English
The span of a subset is the union, over all natural numbers n, of the sets of finite linear combinations using at most n terms from the subset.
Русский
Порожденное подмножество является объединением по всем натуральным числам n множеств конечных линейных комбинаций, использующих не более n элементов из подмножества.
LaTeX
$$$\operatorname{span}_R s = \bigcup_{n\in\mathbb{N}}\{\sum_{i=1}^n r_i\cdot a_i : a_i\in s, r_i\in R\}$$$
Lean4
/-- The span of a subset `s` is the union over all `n` of the set of linear combinations of at most
`n` terms belonging to `s`. -/
theorem span_eq_iUnion_nat (s : Set M) :
(Submodule.span R s : Set M) =
⋃ (n : ℕ), (fun (f : Fin n → (R × M)) ↦ ∑ i, (f i).1 • (f i).2) '' ({f | ∀ i, (f i).2 ∈ s}) :=
by
ext m
simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set']
refine exists_congr (fun n ↦ ⟨?_, ?_⟩)
· rintro ⟨f, g, rfl⟩
exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩
· rintro ⟨f, hf, rfl⟩
exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩
