# 完備度量空間：以最小正距離證明有限度量空間完備，並以 (0,1] 對照

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-complete-metric-space/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-complete-metric-space-01 · production-20261019-adopted-96



## 目標與範圍

證明：每個至少有一點的有限度量空間 (X,d) 都是完備的（單點情形直接成立；至少兩點時用最小正距離 δ 證明每個 Cauchy 序列最終常值）。在 X0={0,1,3}、d(x,y)=|x−y| 上算出 δ=1，給一個最終常值證書與一個明示的非 Cauchy 序列；最後證明子空間 Y=(0,1] 不完備：x_n=1/n 在 Y 中是 Cauchy，但在 Y 中沒有極限。

只在 MKO 的範圍內：有限證書用完整有限度量表且至少一點；最小正距離論證用至少兩點（假設 a1）；序列題只接受明示的最終常值證書或明示的非 Cauchy 反例，有限前綴不冒充完備證明（假設 a2）。(0,1] 的對照用倒數序列的界作完整證書。不處理一般完備化或 Banach 空間；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- metric_def
- order_basics
- abs_rules
- archimedean
- min_finite


- G1 — (X,d) 是有限度量空間，X 至少有一點，度量表完整。
- G2 — 例子：X0={0,1,3}，d(x,y)=|x−y|（ℝ 的通常距離限制在 X0 上）。
- G3 — 對照：Y=(0,1]={t∈ℝ : 0<t≤1}，d(s,t)=|s−t|；序列 x_n=1/n（n≥1）。


- (X,d) — 有限度量空間
- (x_n) — X 中的序列，n=1,2,3 等
- \delta — 最小正距離 min{d(x,y): x≠y}
- N — Cauchy 或收斂定義中的指標門檻
- X_0 — 例子 {0,1,3}，d(x,y)=|x−y|
- Y — 子空間 (0,1]，d(s,t)=|s−t|





## 規則與來源


- metric_def · prerequisite — 度量：d:X×X→ℝ 滿足 d(x,y)≥0 且 d(x,y)=0 ⇔ x=y；d(x,y)=d(y,x)；三角不等式 d(x,z)≤d(x,y)+d(y,z)。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- archimedean · prerequisite — 阿基米德性質：對任意實數 x，存在自然數 n>x；因此對任意 ε>0，存在 n 使 1/n<ε。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mko_complete_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：度量空間 (X,d) 完備，若 X 內每個 Cauchy 序列都收斂到 X 內某點。有限空間至少有兩點時，有限非空的正距離集合有最小值，迫使 Cauchy 尾段最終常值；單點情形所有序列本已常值，不需未定義的最小正距離。抽樣若干序列不足以證一般完備性。原始引文與 canonical MKO 保留。 · mko-complete-metric-space
- mko_cauchy_def · cited — 序列(x_n)為Cauchy，若對每個epsilon>0存在N，使所有m,n>=N都有d(x_m,x_n)<epsilon。定義不先假設極限存在或位於空間內。 · mko-cauchy-sequence
- mko_conv_def · cited — 序列x_n在度量空間中收斂到x，若對每個epsilon>0存在N，使所有n≥N都有d(x_n,x)<epsilon。有限樣本尾段通過不足以證一般收斂；明示最終常值的無限序列則可給完整witness。 · mko-metric-convergence
- min_finite · prerequisite — 非空有限實數集合有最小元素，而且最小元素屬於該集合。
- L_small_dist · lemma — 設有限度量空間至少有兩點，δ=min{d(x,y) : x≠y}。則 δ>0，且 d(x,y)<δ 推出 x=y。
- L_limit_unique · lemma — 在度量空間中，若 x_n→L 且 x_n→L′，則 L=L′。





## 逐步主鏈

S01 · definition操作前

(X,d)\ \text{complete}

操作後

\forall (x_n)\subseteq X\ \text{Cauchy}\ \exists L\in X:\ x_n\to L

條件：無

規則：mko_complete_def · 依賴：G1, mko_cauchy_def, mko_conv_def

葉節點依據：mko_complete_def + mko_cauchy_def + mko_conv_def + def_unfold

依 MKO，完備是空間的性質：X 中每一個 Cauchy 序列都必須收斂到 X 中的某點。Cauchy 的定義不預設極限存在；收斂要求對每個 ε>0 都有門檻 N。所以證明必須對任意 Cauchy 序列成立，不能只測幾條。



S02 · case_split操作前

|X|\ge 1

操作後

|X|=1\ \lor\ |X|\ge 2

條件：無

規則：case_analysis · 依賴：G1

葉節點依據：case_analysis + order_basics

X 至少有一點，所以恰有兩種情況：只有一點，或至少兩點。最小正距離只在至少兩點時有定義（MKO 假設 a1），所以分開處理。



S03 · implies操作前

X=\{p\}

操作後

x_n=p\ \forall n,\ d(x_n,p)=0<\varepsilon\ \Rightarrow\ x_n\to p\in X

條件：|X|=1

規則：mko_conv_def · 依賴：S01, S02, metric_def

葉節點依據：mko_conv_def + metric_def + forall_intro

單點情形：X 中任何序列的每一項都是 p，d(x_n,p)=d(p,p)=0。對每個 ε>0 取 N=1，所有 n≥1 都有 0<ε，所以序列收斂到 p∈X。每個 Cauchy 序列（其實是每個序列）都收斂，X 完備。



S04 · definition操作前

D=\{d(x,y): x,y\in X,\ x\neq y\}

操作後

\delta=\min D

條件：|X|\ge 2

規則：def_intro · 依賴：S02, G1, min_finite

葉節點依據：def_intro + min_finite

至少兩點時，D 非空（有一對相異點）且有限（度量表有限），所以最小值 δ 存在並屬於 D。這是 MKO 所說的最小正距離。



S05 · theorem_application操作前

\delta=\min D

操作後

\delta>0,\ d(x,y)<\delta\Rightarrow x=y

條件：|X|\ge 2

規則：L_small_dist · 依賴：S04

葉節點依據：L_small_dist

依引理 L_small_dist（S05.1、S05.2 證明）：δ 是正數，而且距離小於 δ 的兩點必相同。這是整個證明的關鍵。



S06 · implies操作前

(x_n)\ \text{Cauchy in}\ X,\ \varepsilon=\delta>0

操作後

\exists N\ \forall m,n\ge N:\ d(x_m,x_n)<\delta

條件：\delta>0

規則：forall_elim · 依賴：S01, S05, mko_cauchy_def

葉節點依據：forall_elim + mko_cauchy_def

取 X 中任意一個 Cauchy 序列。Cauchy 的定義對每個 ε>0 都成立，特別是對 ε=δ（S05 保證 δ>0）：存在 N，使所有 m,n≥N 都有 d(x_m,x_n)<δ。



S07 · implies操作前

d(x_N,x_n)<\delta\ \ (n\ge N)

操作後

x_n=x_N\ \ \text{for all}\ n\ge N

條件：無

規則：L_small_dist · 依賴：S05, S06

葉節點依據：L_small_dist + forall_elim

在 S06 中取 m=N：對所有 n≥N，d(x_N,x_n)<δ，依引理 x_n=x_N。所以序列從第 N 項起恆等於 x_N：Cauchy 尾段最終常值。



S08 · implies操作前

L=x_N\in X,\ \varepsilon>0

操作後

\forall n\ge N:\ d(x_n,L)=0<\varepsilon\ \Rightarrow\ x_n\to L

條件：無

規則：mko_conv_def · 依賴：S07, metric_def, mko_conv_def

葉節點依據：mko_conv_def + metric_def + forall_intro

令 L=x_N，它是 X 的點。對任意 ε>0，用同一個 N：n≥N 時 d(x_n,L)=d(x_N,x_N)=0<ε。所以 x_n→L，且極限在 X 中。這就是 MKO 所說的「明示最終常值」完整證書。



S09 · implies操作前

(x_n)\ \text{an arbitrary Cauchy sequence in}\ X

操作後

\text{every Cauchy sequence in}\ X\ \text{converges in}\ X\ \ (|X|\ge 2)

條件：|X|\ge 2

規則：forall_intro · 依賴：S06, S07, S08

葉節點依據：forall_intro

S06 到 S08 對任意 Cauchy 序列成立，沒有對它加任何額外假設，所以依全稱推廣，至少兩點的有限度量空間中每個 Cauchy 序列都在 X 中收斂。



S10 · implies操作前

|X|=1\ \lor\ |X|\ge 2

操作後

(X,d)\ \text{complete}

條件：無

規則：case_analysis · 依賴：S01, S02, S03, S09

葉節點依據：case_analysis + mko_complete_def

兩種情況都證得每個 Cauchy 序列在 X 中收斂（S03、S09），依 S01 的定義，每個至少一點的有限度量空間都完備。



S11 · implies操作前

d(0,1),\ d(0,3),\ d(1,3)

操作後

1,\ 3,\ 2;\ \delta=\min(1,3,2)=1

條件：無

規則：numeric_evaluation · 依賴：G2, S04

葉節點依據：numeric_evaluation + abs_rules + min_finite

X0 的三對相異點距離為 |0−1|=1、|0−3|=3、|1−3|=2，所以 D={1,2,3}，δ=1。d 是 ℝ 的通常距離限制在 X0 上，所以是度量；X0 由 S10 完備。



S12 · implies操作前

x_1=0,\ x_2=3,\ x_n=1\ (n\ge 3)

操作後

(x_n)\ \text{Cauchy with}\ N=3,\ x_n\to 1\in X_0

條件：無

規則：mko_conv_def · 依賴：S11, mko_cauchy_def, mko_conv_def

葉節點依據：mko_conv_def + mko_cauchy_def + forall_intro

這是一個明示的最終常值證書：序列宣告第 3 項以後全部等於 1。對每個 ε>0 取 N=3：m,n≥3 時 d(x_m,x_n)=0<ε（Cauchy），d(x_n,1)=0<ε（收斂到 1）。前兩項不影響結論。



S13 · implies操作前

x_n=0\ (n\ \text{odd}),\ x_n=1\ (n\ \text{even})

操作後

\text{not Cauchy: for}\ \varepsilon=\tfrac12,\ d(x_N,x_{N+1})=1\ge\tfrac12\ \forall N

條件：無

規則：quantifier_negation · 依賴：G2, mko_cauchy_def

葉節點依據：quantifier_negation + mko_cauchy_def

交替序列 0、1、0、1 等：對 ε=1/2，任給 N，取 m=N、n=N+1，兩項一個是 0、一個是 1，距離 1≥1/2。所以「存在 N 使所有 m,n≥N 距離小於 1/2」為假，序列不是 Cauchy。它也不收斂，但這不否證完備性，因為完備只要求 Cauchy 序列收斂。



S14 · implies操作前

x_n=\tfrac1n\in Y,\ \varepsilon>0

操作後

\exists N:\ \forall m,n\ge N,\ \left|\tfrac1m-\tfrac1n\right|<\tfrac1N<\varepsilon

條件：無

規則：archimedean · 依賴：G3, mko_cauchy_def, archimedean

葉節點依據：archimedean + abs_rules + order_basics + forall_intro

每個 1/n 都在 (0,1]，所以序列在 Y 中。給 ε>0，依阿基米德性質取 N 使 1/N<ε。若 m,n≥N，則 1/m 與 1/n 都在 (0,1/N]；兩個正數之差的絕對值小於較大者，所以 |1/m−1/n|<max(1/m,1/n)≤1/N<ε。故 (x_n) 在 Y 中是 Cauchy。



S15 · implies操作前

\left|\tfrac1n-0\right|=\tfrac1n

操作後

x_n\to 0\ \text{in}\ \mathbb{R}

條件：無

規則：mko_conv_def · 依賴：G3, archimedean, mko_conv_def

葉節點依據：mko_conv_def + archimedean + abs_rules

在 ℝ 中：給 ε>0，取 N 使 1/N<ε，則 n≥N 時 |1/n−0|=1/n≤1/N<ε。所以 x_n 在 ℝ 中收斂到 0，而 0∉Y。



S16 · theorem_application操作前

x_n\to L,\ x_n\to L'

操作後

L=L'

條件：無

規則：L_limit_unique · 依賴：metric_def

葉節點依據：L_limit_unique

引理 L_limit_unique（S16.1、S16.2 證明）：度量空間中的極限唯一。下一步需要它把 Y 中的極限與 ℝ 中的極限 0 連起來。



S17 · implies操作前

x_n\to L\ \text{in}\ Y\ \text{for some}\ L\in Y

操作後

L=0\notin Y\ \Rightarrow\ Y\ \text{not complete}

條件：無

規則：contradiction · 依賴：S14, S15, S16, G3

葉節點依據：contradiction + quantifier_negation + L_limit_unique

假設 x_n 在 Y 中收斂到某個 L∈Y。Y 的距離就是 ℝ 的距離，所以 x_n 在 ℝ 中也收斂到 L；由 S15 與引理 L_limit_unique，L=0，但 0∉Y，矛盾。故 Cauchy 序列 (x_n)（S14）在 Y 中沒有極限，Y 不完備。序列在外圍空間 ℝ 有極限並不使子空間完備。







## 局部子步與引理

S05.1 · implies操作前

\delta\in D

操作後

\delta>0

條件：無

規則：metric_def · 依賴：S04, metric_def, min_finite

葉節點依據：metric_def + min_finite + order_basics

δ 屬於 D，所以 δ=d(x0,y0) 對某對相異點 x0≠y0。度量的分離性給 d(x0,y0)≥0 且不為 0，所以 δ>0。



S05.2 · equivalent操作前

x\neq y\Rightarrow d(x,y)\in D\Rightarrow d(x,y)\ge\delta

操作後

d(x,y)<\delta\Rightarrow x=y

條件：無

規則：contrapositive · 依賴：S04, min_finite, contrapositive

葉節點依據：contrapositive + min_finite + order_basics

若 x≠y，則 d(x,y) 是 D 的元素，不小於最小值 δ。取逆否：d(x,y)<δ 推出 x=y。S05.1 與 S05.2 合起來證得引理 L_small_dist。



S16.1 · implies操作前

d(x_n,L)<\varepsilon\ (n\ge N_1),\ d(x_n,L')<\varepsilon\ (n\ge N_2)

操作後

d(L,L')<2\varepsilon\ \ \text{for every}\ \varepsilon>0

條件：無

規則：metric_def · 依賴：metric_def, mko_conv_def

葉節點依據：metric_def + mko_conv_def + order_basics

給 ε>0，由兩個收斂各得 N1、N2；取 n=max(N1,N2)。依對稱與三角不等式，d(L,L′)≤d(L,x_n)+d(x_n,L′)<ε+ε=2ε。



S16.2 · implies操作前

d(L,L')<2\varepsilon\ \forall\varepsilon>0

操作後

L=L'

條件：無

規則：contradiction · 依賴：S16.1, metric_def, contradiction

葉節點依據：contradiction + metric_def + order_basics

若 L≠L′，則 r=d(L,L′)>0；取 ε=r/2 得 r<r，矛盾。所以 L=L′。S16.1 與 S16.2 合起來證得引理 L_limit_unique。







## 逐步反向審查


- S17 · sufficient_goal_reduction · S14, S15, S16, contradiction — 目標 G：Y 不完備。足夠條件 H：存在 Y 中的 Cauchy 序列在 Y 中不收斂；H⇒G 由完備的定義（否定全稱只需一個反例）。H 由 S14 到 S16 正向證成。
- S16.2 · premise_audit · S16.1, metric_def, contradiction — 用到分離性：相異點距離為正；此子步不使用 L_limit_unique。
- S16.1 · premise_audit · metric_def, mko_conv_def — 需要一個同時大於兩個門檻的 n；此子步不使用 L_limit_unique。
- S16 · premise_audit · metric_def, L_limit_unique — 只需度量公理；對任何度量空間成立。
- S15 · premise_audit · archimedean, mko_conv_def — 這是在外圍空間 ℝ 中的收斂；它本身不說明 Y 是否完備。
- S14 · premise_audit · archimedean, mko_cauchy_def, abs_rules — 用到「兩正數之差小於較大者」與阿基米德性質；這是對所有 ε 的倒數序列界證書，N6 只是有限範圍內的核對。
- S13 · premise_audit · mko_cauchy_def, quantifier_negation — 否定「∀ε∃N∀m,n」只需一個 ε 與對每個 N 的一組反例；這是明示的非 Cauchy 反例。
- S12 · premise_audit · mko_cauchy_def, mko_conv_def — 證書依賴「之後所有項都等於 1」這個明示宣告，而不是列出的有限前綴。
- S11 · premise_audit · G2, numeric_evaluation — 完整距離表的三對都計算了；漏掉一對可能算錯 δ。
- S10 · sufficient_goal_reduction · S01, S02, S03, S09, case_analysis — 目標 G：X 完備。足夠條件 H：兩種情況下每個 Cauchy 序列都收斂於 X；H⇒G 由定義與分情況論證。H 由 S03、S09 正向證成。
- S09 · premise_audit · S06, S07, S08, forall_intro — 全稱推廣的條件是序列為任意取；這裡沒有使用任何特定序列。
- S08 · premise_audit · S07, metric_def, mko_conv_def — 同一個 N 對所有 ε 都可用，因為尾段距離恰為 0；L∈X 因為它是序列的一項。
- S07 · premise_audit · S05, S06 — 需要 m=N 在 m≥N 的範圍內；結論只關於 n≥N 的項，前面的項可以任意。
- S06 · premise_audit · mko_cauchy_def, S05, forall_elim — 全稱消去需要 δ 在 ε 的範圍內，即 δ>0；不宣稱反向。
- S05.2 · inverse_equivalence · contrapositive — 命題與其逆否等價，雙向成立。此子步不使用 L_small_dist。
- S05.1 · premise_audit · metric_def, min_finite — 用到最小值被取到；若只是下確界而不被取到，可能是 0。此子步不使用 L_small_dist。
- S05 · premise_audit · S04, L_small_dist — 引理的前提是有限且至少兩點；S04 已提供。
- S04 · premise_audit · S02, min_finite — 需要有限與非空兩個條件；無限空間中這樣的最小值可能不存在（例如 Y 的距離可任意小）。
- S03 · premise_audit · S02, metric_def, mko_conv_def — 只用 d(p,p)=0；這個情況不需要最小正距離。
- S02 · premise_audit · G1, case_analysis — 兩種情況涵蓋所有至少一點的有限集合，且互斥。
- S01 · premise_audit · mko_complete_def, mko_cauchy_def, mko_conv_def — 此步只展開三個定義，不推出新事實。





## 錯誤控制與反例

完備是空間性質，不是測幾條序列MKO 指出的常見誤解是測過幾條序列都收斂就宣稱完備。在 Y=(0,1] 中，常數序列 1/2 與序列 1/2+1/(2n) 等都收斂於 Y，但 1/n 不收斂於 Y（S17）。完備必須對每一個 Cauchy 序列成立；有限空間的證明（S06 到 S09）就是對任意 Cauchy 序列進行的。

外圍空間的極限不算數1/n 在 ℝ 中收斂到 0，但 0∉(0,1]，所以 (0,1] 不完備。反過來，X0={0,1,3} 完備是由 S10 的有限論證得到，而不是因為 ℝ 完備。完備性要求極限屬於這個空間本身。

有限前綴不是證書列出一個序列的前 1000 項都等於 1，並不說明之後的項也是 1。MKO 只接受明示「之後所有項都等於尾值」的最終常值證書（S12）或明示的非 Cauchy 反例（S13）。同理，δ 必須由完整距離表的每一對求出（S11）。


- (0,1] 完備，因為 1/n 在 ℝ 中有極限 0 → reject — 0∉(0,1]，而極限唯一，所以 1/n 在 (0,1] 中沒有極限。
- X0 中交替序列 0、1、0、1 等不收斂，所以 X0 不完備 → reject — 它不是 Cauchy（S13）；完備只要求 Cauchy 序列收斂。
- 在 (0,1] 中測了五條 Cauchy 序列都收斂於 (0,1]，所以 (0,1] 完備 → reject — 1/n 是 (0,1] 中的 Cauchy 序列，在 (0,1] 中沒有極限。
- 有限度量空間中的 Cauchy 序列從第一項起就是常數 → reject — 序列 0、3、1、1、1 等在 X0 中是 Cauchy，但前兩項不同；只能保證最終常值。





## 結論與限制

每個至少一點的有限度量空間都完備：單點時每個序列恆等；至少兩點時取最小正距離 δ>0，Cauchy 定義用 ε=δ 迫使序列從某個 N 起恆等於 x_N，因而收斂到 x_N∈X。X0={0,1,3} 的 δ=1；序列 0、3、1、1、1 等以 N=3 為最終常值證書；交替的 0、1 不是 Cauchy。子空間 (0,1] 不完備：1/n 是 Cauchy，但唯一可能的極限 0 不在 (0,1] 中。


- N6 只在 1≤m,n≤30 的有限範圍核對 |1/m−1/n|<1/min(m,n)；對所有 m,n 的證明是 S14 的論證。
- min_finite 是本稿的前提；錯誤控制中 1/2+1/(2n) 收斂於 Y 只作說明，未列為編號步驟。





## 驗證及來源綁定

7 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: f777d86bce746681448ac94bc6f723103abd39b7d9520aa52006b6c641835c8d
- original source SHA-256: 1db5dbc4b9d2cc946ce1390b35ee86de434aefd9ce839d023e2612e22357f1e8
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-complete-metric-space-01.json)