# 實向量子空間

實向量空間的非空子集若含零向量並對向量加法與每個實純量乘法封閉，則為向量子空間。

mko-vector-subspace · definition · v0.10.0



## 數學敘述

本輪只處理R²中的零空間、全空間、過原點直線與明示有限反例。正例使用齊次線性方程或span的全稱代數證書；有限抽樣通過不足以證子空間。





## 代表公式（精確 TeX）

U(V)





## 成立條件


- 母空間固定為R²並使用通常向量運算。
- 正例證書須全稱涵蓋加法及任意實純量；仿射直線不經原點不是子空間。





## 符號作用域


- U — 候選子空間
- V — 母向量空間





## 直觀、定義與常見誤解

含零向量是必要條件。

過原點齊次直線可由線性方程給全稱封閉證書。

一個反例足以否證；有限正樣本不足以證明。

把任意直線或有限抽樣封閉當成子空間證書。





## 已採用的推導導讀

[以全稱封閉認證過原點直線](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-vector-subspace-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [實向量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-vector-space/) — 提供R²向量運算與純量。
- [子集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) — 子空間是母空間子集。
- [量詞與明示論域](https://ocme.evemisslab.com/zh-Hant/mko/mko-quantifier/) — 封閉性是全稱責任。





## 驗證界線

只在R²與明示證書範圍重算，不外推任意維或未知運算。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入核、像、維度與商向量空間。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/vector-subspace.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector-subspace/index.md)