# 範數誘導度量

同一實賦範向量空間上的範數以向量差的範數定義度量，度量公理由範數公理全稱推出。

mko-norm-induced-metric · definition · v0.10.0



## 數學敘述

若(V,norm)為已認證的實賦範向量空間，則d(x,y)=norm(x-y)滿足非負、分離、對稱與三角不等式。本輪只在R^n的命名l1與linfinity範數作精確座標切片。





## 代表公式（精確 TeX）

D(x,y)





## 成立條件


- 左右點位於同一有限維實座標空間，使用同一已命名範數。
- 誘導性來自全稱公式與範數公理，不由有限點距離樣本建立。





## 符號作用域


- d — 範數誘導度量
- V — 實賦範向量空間
- x — 第一向量
- y — 第二向量





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

分離性由norm(x-y)=0當且僅當x-y=0。

對稱性由norm(-(y-x))=norm(y-x)。

三角不等式由x-z=(x-y)+(y-z)及範數三角不等式。

檢查有限幾對距離後就宣稱任意metric由某個norm誘導。





## 已採用的推導導讀

[範數誘導度量：由範數公理證明 d(x,y)=‖x−y‖ 是度量，並在 ℝ³ 上以 l1 與 l∞ 精確計算](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-norm-induced-metric-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [實賦範向量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-normed-vector-space/) — 誘導公式依已認證範數。
- [度量空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-metric-space/) — 結論是度量公理。
- [固定基底下的平面向量](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector/) — 誘導公式使用同一空間中的向量差。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — d須為V乘V到非負實數的總函數。





## 驗證界線

只處理同一認證範數的誘導公式；不宣稱每個度量皆範數誘導，也不推出完備、內積、緊緻或有限維。

not_formalized

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





## 下一個義務

與完備度量空間共同支撐實Banach空間。





## 同源結構化資料

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

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