English
If s is a subset of V, then the affine span of s lies inside the affine subspace determined by the linear span of s.
Русский
Если s — подмножество V, то аффинный охват s лежит внутри аффинного подпроизвольного пространства, соответствующего линейному охвату s.
LaTeX
$$$\operatorname{affineSpan} k s \le (\operatorname{Submodule.span} k s).toAffineSubspace$$$
Lean4
/-- When the affine space is also a vector space, the affine span is contained within the linear
span. -/
theorem affineSpan_le_toAffineSubspace_span {s : Set V} : affineSpan k s ≤ (Submodule.span k s).toAffineSubspace :=
by
intro x hx
simp only [SetLike.mem_coe, Submodule.mem_toAffineSubspace]
induction hx using affineSpan_induction' with
| mem x hx => exact Submodule.subset_span hx
| smul_vsub_vadd c u _ v _ w _ hu hv hw =>
simp only [vsub_eq_sub, vadd_eq_add]
apply Submodule.add_mem _ _ hw
exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)
