affineSpan_subset_span — Mathlib

English

For any set s, the underlying set of the affine span is contained in the linear span of s.

Русский

Для любого множества s их аффинный охват как подмножество содержится в линейном охвате s.

LaTeX

$$$(\operatorname{affineSpan} k s : \operatorname{Set} V) \subseteq \operatorname{Submodule.span} k s$$$

Lean4

theorem affineSpan_subset_span {s : Set V} : (affineSpan k s : Set V) ⊆ Submodule.span k s :=
  affineSpan_le_toAffineSubspace_span

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