English
For any subset s of M, the additive submonoid generated by s equals the closure of s under addition, obtained by closing under all linear combinations with natural number coefficients.
Русский
Для любого множества s в M порождаемая аддитивная подмоноидальная часть совпадает с замыканием s по сложению, т.е. получаем замыкание под действием натуральных коэффициентов.
LaTeX
$$$$(\operatorname{span} R s).\text{toAddSubmonoid} = \operatorname{closure}( {\{ r\cdot x : r\in R, x\in s\} } )$$$$
Lean4
theorem span_eq_closure {s : Set M} : (span R s).toAddSubmonoid = closure (@univ R • s) :=
by
refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)
case of_mem_span =>
induction hx using span_induction with
| mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
| zero => exact zero_mem _
| add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
| smul r₁ y _h hy =>
clear _h
induction hy using closure_induction with
| mem _ h =>
obtain ⟨r₂, -, x, hx, rfl⟩ := h
exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
| zero => simp only [smul_zero, zero_mem]
| add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂
case of_mem_closure =>
refine closure_le.2 ?_ hx
rintro - ⟨r, -, x, hx, rfl⟩
exact smul_mem _ _ (subset_span hx)
