Conditions for a subspace (LADR 1.34)

• Conditions for a subspace (LADR 1.34) #Card
  • 部分集合 $U\subseteq V$ が部分空間であるための必要十分条件（実用的判定法）は？

Back

命題. $U\subseteq V$ が $V$ の部分空間 $\iff$ 次の3条件を満たす：

1. 加法単位元: $0\in U$
2. 加法で閉じる: $u,w\in U \Rightarrow u+w\in U$
3. スカラー倍で閉じる: $a\in\mathbf{F},\ u\in U \Rightarrow au\in U$

手筋: 部分空間判定はこの3点を確認するのが最速。加法逆元は条件3（$-u=(-1)u$）から自動。 条件1は「$U\neq\varnothing$」に置き換え可能だが、実際は $0\in U$ を示すのが最も速い。

Lean

Submodule の場（zero_mem', add_mem', smul_mem'）がちょうどこの3条件。 判定補題 Submodule.mem_*、AddSubmonoid への落とし込み。