affineSpan_insert_zero — Mathlib

English

The affine span of insert 0 s is exactly the linear span of s.

Русский

Аффинный охват вставки 0 в s равен линейному охвату s.

LaTeX

$$$(\operatorname{affineSpan} k (\mathrm{insert}\ 0\ s) : \operatorname{Set} V) = \operatorname{Submodule.span} k s$$$

Lean4

theorem affineSpan_insert_zero (s : Set V) : (affineSpan k (insert 0 s) : Set V) = Submodule.span k s :=
  by
  rw [← Submodule.span_insert_zero]
  refine affineSpan_subset_span.antisymm ?_
  rw [← vectorSpan_add_self, vectorSpan_def]
  refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..
  gcongr
  exact subset_sub_left <| mem_insert ..

Похожие утверждения