Dimension of a subspace (LADR 2.37)

• Dimension of a subspace (LADR 2.37) #Card
  • 有限次元 $V$ の部分空間 $U$ について $\dim U$ と $\dim V$ の関係は？証明の一行は？

Back

命題. $V$ が有限次元、$U$ が部分空間なら $\dim U\le\dim V$。

証明: $U$ の基底は $V$ の中の線形独立リスト、$V$ の基底は生成リスト。よって cards/linear-algebra/prop-2-22（独立 ≤ 生成）で即座に従う。∎

セット: 等号の場合は $U=V$（cards/linear-algebra/prop-2-39）。

Lean

Submodule.finrank_le。