# 三點離散空間的全部點對分離

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

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

derivation-mko-hausdorff-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

完整核三點離散空間的 Hausdorff 性，並對照一個失敗點對。

有限全枚舉；不把有限 Hausdorff 推離散的結論外推。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau=P(X)；對照拓撲 sigma={空集,{a},{a,b},X}。


- \mathcal N(x) — 全部開鄰域
- \tau,\sigma — 兩個指定拓撲





## 規則與來源


- mko_definition · cited — 必須forall x≠y存在open U,V，使x∈U、y∈V且U∩V=empty。一個失敗pair即可證non-Hausdorff；有限sample成功不足以證一般空間。本輪完整有限topology exhaustive驗證。empty與singleton vacuously Hausdorff；finite Hausdorff implies discrete不可外推至infinite spaces。 · mko-hausdorff-space
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — Hausdorff：每對異點各有包含該點的不交開鄰域；點的開鄰域為含該點的開集。





## 逐步主鏈

S01 · implies操作前

\tau=\{\varnothing,\{a\},\{b\},\{c\},\{a,b\},\{a,c\},\{b,c\},X\}

操作後

\tau\text{ is a topology}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

八個子集全列，聯交仍是子集。



S02 · implies操作前

x\ne y\in X

操作後

\{\{a,b\},\{a,c\},\{b,c\}\}\text{ are all unordered pairs}

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

三點有且只有這三個無序異點對。



S03 · implies操作前

(x,y)=(a,b)

操作後

U=\{a\},\ V=\{b\},\ U\cap V=\varnothing

條件：無

規則：sets · 依賴：S01, S02

葉節點依據：sets

兩個單點集均開並含正確點。



S04 · implies操作前

(x,y)=(a,c)

操作後

U=\{a\},\ V=\{c\},\ U\cap V=\varnothing

條件：無

規則：sets · 依賴：S01, S02

葉節點依據：sets

第二點對使用對應的開單點見證。



S05 · implies操作前

(x,y)=(b,c)

操作後

U=\{b\},\ V=\{c\},\ U\cap V=\varnothing

條件：無

規則：sets · 依賴：S01, S02

葉節點依據：sets

第三點對亦分離，至此沒有未核異點對。



S06 · definition操作前

\forall x\ne y\ \exists U,V\text{ disjoint open neighborhoods}

操作後

(X,\tau)\text{ is Hausdorff}

條件：無

規則：definition_here · 依賴：S02, S03, S04, S05

葉節點依據：definition_here

以上三項和交換對稱性完成定義。



S07 · definition操作前

\sigma=\{\varnothing,\{a\},\{a,b\},X\}

操作後

\mathcal N_\sigma(c)=\{X\},\quad\mathcal N_\sigma(a)=\{\{a\},\{a,b\},X\}

條件：無

規則：definition_here · 依賴：G1

葉節點依據：definition_here

對照族是含兩端的鏈拓撲；列出 c 與 a 的全部開鄰域。



S08 · implies操作前

U\in\mathcal N_\sigma(c),\quad V\in\mathcal N_\sigma(a)

操作後

U\cap V=V\ne\varnothing

條件：無

規則：sets · 依賴：S07

葉節點依據：sets

c 只能取 X，故與 a 的任何開鄰域都相交，sigma 非 Hausdorff。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S07 — 一個完整失敗點對足以否定全稱性。
- S07 · premise_audit · G1 — 這個失敗點對有完整鄰域枚舉，不是選壞一對見證。
- S06 · premise_audit · S02, S03, S04, S05 — 空與單點空間則沒有異點對，條件真。
- S05 · premise_audit · S01, S02 — 全稱成立來自全部點對而非若干成功。
- S04 · premise_audit · S01, S02 — 見證都在完整拓撲內。
- S03 · premise_audit · S01, S02 — 不僅不交，也逐一核點的包含。
- S02 · premise_audit · G1 — 反向有序對可交換見證，不需重複另一證明。
- S01 · premise_audit · G1 — 清單是完整冪集，不是樣本。





## 錯誤控制與反例

點對完整性列完整無序異點對再交換方向。

失敗證書非 Hausdorff 需一個點對的所有鄰域選擇都失敗。


- 成功分離一對就證 Hausdorff。 → reject — 定義需每一異點對。
- 只選一組相交鄰域就證非 Hausdorff。 → reject — 必須排除該點對的所有不交見證；S07 完整列出才足夠。
- 所有無限 Hausdorff 空間也離散。 → reject — 通常實數線 Hausdorff，但單點不開。





## 結論與限制

離散 tau 為 Hausdorff；鏈拓撲 sigma 由 (a,c) 點對證非 Hausdorff。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e8794925db0c4d7267f7a0f2001404f5c259749d819b000219306b1c0f6dd12d
- original source SHA-256: e8794925db0c4d7267f7a0f2001404f5c259749d819b000219306b1c0f6dd12d
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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