# Excluding every nontrivial clopen set

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-connected-topological-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-connected-topological-space-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Decide connectedness of a three-point chain topology.

Complete finite enumeration, with the empty-space connected convention and no graph connectivity.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau={empty,{a},{a,b},X}; connected means no two disjoint nonempty opens cover X.


- U,V — candidate separation
- \mathcal F — all closed sets





## Rules and sources


- mko_definition · cited — In a complete finite topology, enumerate all candidate separations or clopen subsets. Disconnectedness requires an explicit witness and connectedness requires excluding every one. The empty space is connected under the declared vacuous convention, and every singleton space is connected. Do not conflate this with graph connectivity. · mko-connected-topological-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 — Closed sets complement opens; connectedness means no two nonempty disjoint opens have union equal to the whole space.





## Main derivation

S01 · impliesBefore

\varnothing\subset\{a\}\subset\{a,b\}\subset X

After

\tau\text{ is a topology}

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

Nonempty unions/intersections of this finite chain take extremal members; empty and whole sets are present.



S02 · definitionBefore

\mathcal F=\{X\setminus U:U\in\tau\}

After

\mathcal F=\{X,\{b,c\},\{c\},\varnothing\}

Conditions: none

Rule: definition_here · Uses: S01

Leaf basis: definition_here

Enumerate all closed sets by complementation.



S03 · equivalentBefore

C\in\tau\cap\mathcal F

After

\tau\cap\mathcal F=\{\varnothing,X\}

Conditions: none

Rule: sets · Uses: S01, S02

Leaf basis: sets

The complements of {a} and {a,b} are not open, leaving no nontrivial clopen set.



S04 · impliesBefore

X=U\cup V,\ U,V\ne\varnothing,\ U\cap V=\varnothing

After

V=X\setminus U

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

In any separation, the second open is exactly the complement of the first.



S05 · impliesBefore

U,V\in\tau,\quad V=X\setminus U

After

U\text{ is nontrivial clopen}

Conditions: none

Rule: sets · Uses: S04

Leaf basis: sets

The two open sides make U closed as well, and nonempty/proper.



S06 · impliesBefore

\tau\cap\mathcal F=\{\varnothing,X\}

After

\text{no separation exists}

Conditions: none

Rule: sets · Uses: S03, S05

Leaf basis: sets

The exhaustive table rules out every nontrivial U required by a separation.



S07 · definitionBefore

\text{no separation of }X

After

X\text{ is connected}

Conditions: none

Rule: definition_here · Uses: S06

Leaf basis: definition_here

Apply the definition; here every nonempty open also contains a, independently excluding disjoint nonempty pairs.



S08 · impliesBefore

|Y|\le1

After

Y\text{ has no two disjoint nonempty parts covering it}

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

Empty and singleton spaces have no separation and are connected under the declared convention.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1 — The boundary argument does not rely on the special point a.
- S07 · premise_audit · S06 — The additional intersection check agrees with the full clopen table.
- S06 · premise_audit · S03, S05 — Failure to find a sampled separation has not been substituted for exhaustive exclusion.
- S05 · premise_audit · S04 — This is the implication from a separation to a clopen witness.
- S04 · premise_audit · G1 — Both disjointness and coverage are required for the complement equality.
- S03 · inverse_equivalence · S01, S02 — All four opens have been compared with the full closed list.
- S02 · premise_audit · S01 — Complements are relative to the fixed X.
- S01 · premise_audit · G1 — A valid topology is established before classifying connectedness.





## Error controls and negative controls

Exclusion is exhaustiveThe full clopen intersection table covers every candidate.

Separate spaces from graphsDo not use a visual vertex/edge impression to classify topological connectedness.


- {a} and {b,c} form an open separation. → reject — {b,c} is not in the topology.
- Three points force disconnectedness. → reject — Connectedness is topological; all separations were excluded.
- A drawing without edges makes this space disconnected. → reject — No graph is specified; its definition cannot replace the topology.





## Result and limitations

The example is connected; only empty and X are clopen.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 1b8193f1601cc4a8e6e1096904a1c68b5c5986760252adb587d348f2d06b617b
- original source SHA-256: 1b8193f1601cc4a8e6e1096904a1c68b5c5986760252adb587d348f2d06b617b
- 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-connected-topological-space-01.json)