Subspaces of finite-dimensional spaces (LADR 2.25)
- Subspaces of finite-dimensional spaces (LADR 2.25) #Card
- 有限次元ベクトル空間の部分空間は有限次元か？証明の構成は？
命題. 有限次元ベクトル空間の任意の部分空間は有限次元。
証明の骨子（貪欲構成）: $U\neq\operatorname{span}(u_1,\dots,u_{k-1})$ である限り $u_k\in U\setminus\operatorname{span}(u_1,\dots,u_{k-1})$ を取り続ける。各段階でリストは線形独立（cards/linear-algebra/prop-2-19 の対偶: どのベクトルも前の span に入らない）。独立リストは $V$ の生成リストより長くなれない（cards/linear-algebra/prop-2-22）から、この過程は有限回で止まり、$U$ は有限リストで生成される。∎
手筋: 「span に入らない限り貪欲に足す→独立性が保たれる→ 2.22 で停止」は基底の存在証明の原型。
Submodule.finiteDimensional（FiniteDimensional F V のインスタンス）。