Span is the smallest containing subspace (LADR 2.6)

• Span is the smallest containing subspace (LADR 2.6) #Card
  • $\operatorname{span}(v_1,\dots,v_m)$ と「$v_1,\dots,v_m$ を含む部分空間」の関係は？

Back

命題. リストの span は、そのリストの全ベクトルを含む $V$ の最小の部分空間。

証明の骨子:

1. span は部分空間（$0=0v_1+\cdots+0v_m$、線形結合同士の和・スカラー倍も線形結合。cards/linear-algebra/prop-1-34）。
2. 各 $v_k\in\operatorname{span}$（$a_k=1$、他 $0$）。
3. $v_1,\dots,v_m$ を含む任意の部分空間は、加法・スカラー倍で閉じるから span を含む。

手筋: 「最小性」は cards/linear-algebra/intersection-of-subspaces（含む部分空間全体の交わり）とも整合。

Lean

Submodule.span_le（span ≤ U ⟺ s ⊆ U、Galois 接続 Submodule.gi）。