Length of linearly independent list ≤ length of spanning list (LADR 2.22)
- Length of linearly independent list ≤ length of spanning list (LADR 2.22) #Card
- 有限次元空間で、線形独立リストの長さと生成リストの長さの間に成り立つ不等式とその証明のアイデアは？
命題. 有限次元ベクトル空間では、任意の線形独立リストの長さ $\le$ 任意の生成リストの長さ。
証明のアイデア（交換論法）: 独立リスト $u_1,\dots,u_m$、生成リスト $w_1,\dots,w_n$。ステップ $k$ で $u_k$ をリストに加えると従属になるので、cards/linear-algebra/prop-2-19（線形従属補題）によりどれかの $w$ を除いて生成性を保てる（$u$ たちは独立なので除かれるのは必ず $w$）。$m$ ステップ完了まで $w$ が尽きないから $m\le n$。
即効の帰結（例 2.23, 2.24）: $\mathbf{R}^3$ で長さ4のリストは独立でない／長さ3のリストは $\mathbf{R}^4$ を生成しない—計算不要。
射程: 基底の長さの不変性（2.34）＝次元の well-definedness の源泉。
LinearIndependent.fintype_card_le_finrank 系。交換補題は exists_linearIndependent 周辺。