# Compactness reduces separating neighborhoods to finitely many

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-compact-subset-closed-in-hausdorff/)

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-compact-subset-closed-in-hausdorff-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Prove a compact subset K of a Hausdorff space is closed.

A general cover proof, not replaced by finite instances and not proving a converse.





## Givens and symbols


- sets
- topology
- hausdorff_def
- compact_def


- G1 — X is Hausdorff and K is compact in its subspace topology.


- U_y,V_y — separating neighborhoods
- m — finite-subcover size





## Rules and sources


- mko_definition · cited — For each x outside K and each y in K, choose disjoint open U_y containing x and V_y containing y. The V_y cover K, so compactness supplies a finite subcover. The corresponding finite intersection of U_y is an open neighborhood of x disjoint from K; therefore X minus K is open. Empty K is closed too. The Hausdorff hypothesis cannot be removed, and closedness does not conversely imply compactness in general. · mko-compact-subset-closed-in-hausdorff
- 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.
- hausdorff_def · prerequisite — Hausdorffness: every distinct pair has disjoint open neighborhoods containing the assigned points.
- compact_def · prerequisite — K is compact when every relative-open cover has a finite original-index subcover; relative opens are intersections of ambient opens with K.





## Main derivation

S01 · case_splitBefore

K=\varnothing

After

X\setminus K=X\text{ is open}

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

Handle empty K first: its complement is the open whole space.



S02 · impliesBefore

K\ne\varnothing,\quad x\in X\setminus K

After

x\ne y\quad\forall y\in K

Conditions: K\ne\varnothing

Rule: sets · Uses: G1

Leaf basis: sets

Fix an arbitrary outside point x; it differs from every y in K.



S03 · theorem_applicationBefore

x\ne y\in K\cup\{x\}

After

x\in U_y,\ y\in V_y,\ U_y,V_y\text{ open},\ U_y\cap V_y=\varnothing

Conditions: none

Rule: hausdorff_def · Uses: G1, S02, hausdorff_def

Leaf basis: hausdorff_def

For each y use Hausdorff separation, retaining both neighborhoods.



S04 · impliesBefore

y\in K\cap V_y\quad(y\in K)

After

K\subseteq\bigcup_{y\in K}(K\cap V_y)

Conditions: none

Rule: sets · Uses: S03

Leaf basis: sets

Each y lies in its own V_y, and intersection with K is relatively open.



S05 · theorem_applicationBefore

(K\cap V_y)_{y\in K}\text{ covers }K

After

K\subseteq\bigcup_{j=1}^{m}V_{y_j},\quad m\in\mathbb N

Conditions: K\ne\varnothing

Rule: compact_def · Uses: G1, S04, compact_def

Leaf basis: compact_def

Compactness selects finitely many original indices; K nonempty permits m≥1.



S06 · impliesBefore

U=\bigcap_{j=1}^{m}U_{y_j}

After

U\text{ is open and }x\in U

Conditions: m<\infty

Rule: topology · Uses: S03, S05

Leaf basis: topology

Finite intersections of opens are open, and every factor contains x.



S07 · impliesBefore

z\in U\cap K

After

z\in V_{y_j}\cap U_{y_j}=\varnothing\text{ for some }j

Conditions: none

Rule: sets · Uses: S03, S05, S06

Leaf basis: sets

A point z in U and K lies in some selected V, while U lies in the corresponding U-neighborhood, a contradiction.



S08 · impliesBefore

\forall x\in X\setminus K\ \exists U_x\text{ open}:x\in U_x\subseteq X\setminus K

After

X\setminus K=\bigcup_{x\notin K}U_x\text{ open};\quad K\text{ closed}

Conditions: none

Rule: topology · Uses: S01, S02, S06, S07

Leaf basis: topology

The complement is the union of these open neighborhoods, hence open; an empty complement is the empty open union.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S01, S02, S06, S07 — This establishes only the forward theorem, not that every closed set is compact.
- S07 · premise_audit · S03, S05, S06 — The index j may depend on z; no single V is assumed to cover K.
- S06 · premise_audit · S03, S05 — The finite-intersection axiom, not arbitrary intersection closure, is used.
- S05 · premise_audit · G1, S04, compact_def — Finiteness is the essential bridge to openness of the next intersection.
- S04 · premise_audit · S03 — No claim is made yet that the intersection of every U_y is open; that could be infinite.
- S03 · premise_audit · G1, S02, hausdorff_def — Neighborhoods for one y alone need not cover K.
- S02 · premise_audit · G1 — Arbitrariness of x will establish openness of the whole complement.
- S01 · premise_audit · G1 — This branch requires no point in K or nonempty subcover.





## Error controls and negative controls

Finite-intersection bridgeSelect finitely many V's before intersecting the corresponding U's.

Pairwise quantifiersSeparate a fixed outside point from every point of K, then release the outside-point quantifier.


- Compact subsets of every topological space are closed. → reject — A singleton in the indiscrete two-point space is compact but not closed.
- The intersection of all U_y is necessarily open. → reject — Only finite intersections are guaranteed open; compactness must be used first.
- Every closed subset of the real line is compact. → reject — R is closed; the cover (-n,n), n≥1, has no finite subcover.





## Result and limitations

Under the two stated hypotheses K is closed, including empty K.







## Verification and source binding

0 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 813fe0a58f2f6c26c88fc29c4ab65d01c638ff0c78dbb769f371543294dd6ab7
- original source SHA-256: 70031bac985789aa1c49e84f0a64049275096117bd97bc22051b96b5a3ce3cac
- 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-compact-subset-closed-in-hausdorff-01.json)