# 度量空間

度量空間由集合與距離函數組成，距離非負、只在相同點為零、對稱且滿足三角不等式。

mko-metric-space · definition · v0.10.0



## 數學敘述

集合X上的度量d:X×X→R滿足非負與分離、對稱及三角不等式。完整有限距離表可逐格及逐三元組核對指定候選。





## 代表公式（精確 TeX）

d(x,y)





## 成立條件


- 題庫使用0到n-1的有限載體及完整整數距離表。
- 有限表驗收只證指定模型，不把窮舉外推到任意無限度量空間。





## 符號作用域


- d — 距離函數候選
- x — 有限載體點
- y — 有限載體點





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

對角線須為零，非對角線不得為零，二者共同構成分離性。

對稱性要求d(i,j)=d(j,i)。

三角不等式必須對每個i,j,k核對d(i,k)≤d(i,j)+d(j,k)。

只核對非負與對稱就叫度量，或漏掉非對角零值與三角不等式。





## 已採用的推導導讀

[度量空間：逐格與逐三元組核對有限距離表](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-metric-space-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 度量有固定載體。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 距離對每個有序點對給唯一實值。
- [二元關係與集合投影](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) — 距離表以點對索引。
- [實數](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-number/) — 距離值為非負實數。
- [實數大小與順序](https://ocme.evemisslab.com/zh-Hant/mko/mko-order-relation/) — 非負與三角不等式使用序。





## 驗證界線

只驗完整有限表；不外推任意函數空間或無限載體。

not_formalized

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





## 下一個義務

加入開球、度量收斂、Cauchy序列與完備性。





## 同源結構化資料

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

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