Sum is the smallest containing subspace (LADR 1.40)
- Sum is the smallest containing subspace (LADR 1.40) #Card
- 部分空間の和 $V_1+\cdots+V_m$ は $V$ の中でどういう位置づけ？
命題. $V_1,\dots,V_m$ が $V$ の部分空間なら、$V_1+\cdots+V_m$ は $V_1,\dots,V_m$ をすべて含む最小の部分空間。
証明の要点. (i) 和は $0$ を含み加法・スカラー倍で閉じる→cards/linear-algebra/prop-1-34 より部分空間。 (ii) 各 $V_k$ は和に含まれる（他を $0$ にとる）。(iii) $V_1,\dots,V_m$ を含む任意の部分空間は それらの有限和を全て含むので和を含む。よって和が最小。
⊔ が束の上限であること自体（Submodule.sup の IsLUB）。sup_le, le_sup_left/right。