# Separating every pair in a discrete three-point space [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-hausdorff-space/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-hausdorff-space-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Exhaustively audit Hausdorffness of a discrete three-point space and contrast a failed pair. Exhaustive finite enumeration; no extrapolation of the finite Hausdorff/discrete corollary. ## Givens and symbols - sets - topology - definition_here - G1 — X={a,b,c}, tau=P(X); contrast sigma={empty,{a},{a,b},X}. - \mathcal N(x) — all open neighborhoods - \tau,\sigma — two specified topologies ## Rules and sources - mko_definition · cited — For every x≠y there must be open U,V containing x,y respectively with U∩V empty. One exhaustively failed pair proves non-Hausdorffness; finitely sampled successes do not certify a general space. This slice exhaustively audits a complete finite topology. Empty and singleton spaces are vacuously Hausdorff. The finite Hausdorff-implies-discrete corollary must not be extrapolated to infinite spaces. · mko-hausdorff-space - sets · prerequisite — Compute unions, intersections, complements, inclusion and preimages element by element. - topology · prerequisite — A topology contains empty and whole sets and is closed under arbitrary unions and finite intersections; a finite family admits exhaustive checks. - definition_here · prerequisite — Hausdorffness: every distinct pair has disjoint open neighborhoods containing the assigned points; an open neighborhood is an open set containing the point. ## Main derivation S01 · impliesBefore \tau=\{\varnothing,\{a\},\{b\},\{c\},\{a,b\},\{a,c\},\{b,c\},X\} After \tau\text{ is a topology} Conditions: none Rule: topology · Uses: G1 Leaf basis: topology All eight subsets are listed and unions/intersections remain subsets. S02 · impliesBefore x\ne y\in X After \{\{a,b\},\{a,c\},\{b,c\}\}\text{ are all unordered pairs} Conditions: none Rule: sets · Uses: G1 Leaf basis: sets These are exactly the three unordered pairs of distinct points. S03 · impliesBefore (x,y)=(a,b) After U=\{a\},\ V=\{b\},\ U\cap V=\varnothing Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets Both singletons are open and contain the assigned points. S04 · impliesBefore (x,y)=(a,c) After U=\{a\},\ V=\{c\},\ U\cap V=\varnothing Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets Use the corresponding open singleton witnesses for the second pair. S05 · impliesBefore (x,y)=(b,c) After U=\{b\},\ V=\{c\},\ U\cap V=\varnothing Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets The third pair is separated, exhausting all distinct pairs. S06 · definitionBefore \forall x\ne y\ \exists U,V\text{ disjoint open neighborhoods} After (X,\tau)\text{ is Hausdorff} Conditions: none Rule: definition_here · Uses: S02, S03, S04, S05 Leaf basis: definition_here The three audits and swapping symmetry establish the definition. S07 · definitionBefore \sigma=\{\varnothing,\{a\},\{a,b\},X\} After \mathcal N_\sigma(c)=\{X\},\quad\mathcal N_\sigma(a)=\{\{a\},\{a,b\},X\} Conditions: none Rule: definition_here · Uses: G1 Leaf basis: definition_here The contrast family is a chain topology with endpoints; list every open neighborhood of c and a. S08 · impliesBefore U\in\mathcal N_\sigma(c),\quad V\in\mathcal N_\sigma(a) After U\cap V=V\ne\varnothing Conditions: none Rule: sets · Uses: S07 Leaf basis: sets c only has X, so every open neighborhood of a meets it; sigma is not Hausdorff. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · S07 — One exhaustively failed pair refutes the universal property. - S07 · premise_audit · G1 — The failed pair has exhaustive neighborhood lists, not merely one badly chosen pair of witnesses. - S06 · premise_audit · S02, S03, S04, S05 — Empty and singleton spaces have no distinct pairs, so the condition is vacuous. - S05 · premise_audit · S01, S02 — The universal result comes from all pairs, not several successes. - S04 · premise_audit · S01, S02 — Both witnesses belong to the complete topology. - S03 · premise_audit · S01, S02 — Both disjointness and containment of the assigned points are checked. - S02 · premise_audit · G1 — Reversing an ordered pair swaps its witnesses. - S01 · premise_audit · G1 — The list is the complete power set, not a sample. ## Error controls and negative controls Pair completenessList all unordered distinct pairs and swap directions. Failure certificateA non-Hausdorff certificate needs all neighborhood choices for one pair to fail. - Separating one pair proves Hausdorffness. → reject — Every distinct pair is required. - One intersecting choice proves non-Hausdorffness. → reject — All disjoint witnesses for that pair must be excluded; the full list at S07 is needed. - Every infinite Hausdorff space is discrete. → reject — The usual real line is Hausdorff but its singletons are not open. ## Result and limitations Discrete tau is Hausdorff; the pair (a,c) proves chain topology sigma is not. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: e8794925db0c4d7267f7a0f2001404f5c259749d819b000219306b1c0f6dd12d - original source SHA-256: e8794925db0c4d7267f7a0f2001404f5c259749d819b000219306b1c0f6dd12d - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-hausdorff-space-01.json)