# 實賦範向量空間

實向量空間配備正定、絕對齊次且滿足三角不等式的實值範數。

mko-real-normed-vector-space · definition · v0.10.0



## 數學敘述

範數把向量送到非負實數，且norm(v)=0當且僅當v=0、norm(a v)=|a| norm(v)、norm(u+v)不超過norm(u)+norm(v)。本輪只使用R^n上的l1與linfinity命名公式。





## 代表公式（精確 TeX）

N(V)





## 成立條件


- 題庫用固定有限維整數座標向量。
- l1與linfinity資格來自公式的全稱代數證書；有限抽樣不冒充一般範數證明。





## 符號作用域


- N — 範數紀錄
- V — 實向量空間





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

l1是座標絕對值總和。

linfinity是座標絕對值最大值。

範數差可誘導兩點距離，但誘導度量另立節點。

以有限點通過非負與三角測試就宣稱任意公式是範數。





## 已採用的推導導讀

[實賦範向量空間：ℓ¹ 與 ℓ^∞ 公式的全稱範數證書，以及兩個非範數公式](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-real-normed-vector-space-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [實向量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-vector-space/) — 範數定義在實向量空間。
- [絕對值](https://ocme.evemisslab.com/zh-Hant/mko/mko-absolute-value/) — 純量齊次使用實數絕對值。
- [實數大小與順序](https://ocme.evemisslab.com/zh-Hant/mko/mko-order-relation/) — 非負與三角不等式依實數順序。





## 驗證界線

只接受命名精確公式；不從抽樣建立範數公理。

not_formalized

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





## 下一個義務

加入範數誘導度量、Banach與有界算子。





## 同源結構化資料

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

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