# Exact boundary comparison with the complement

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-topological-boundary/)

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-topological-boundary-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Compute the boundaries of A={b} and its complement in a chain topology.

Exhaustive finite open/closed-set calculation, without a metric or drawing.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau={empty,{a},{a,b},X}, A={b}, D=X minus A={a,c}.


- \partial A — topological boundary
- D — complement relative to X





## Rules and sources


- mko_definition · cited — After validating the complete finite topology, calculate closure and interior exactly. Retain boundary(A)=boundary(complement A), the empty/whole-set boundaries and dependence on the topology. If a neighborhood-contact criterion is used, every open neighborhood must be considered. · mko-topological-boundary
- 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, closure intersects all closed supersets, interior unites all open subsets, and boundary is closure minus interior.





## 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

In the inclusion chain, unions and intersections of nonempty subfamilies are their largest and smallest members; empty union/intersection are included.



S02 · definitionBefore

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

After

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

Conditions: none

Rule: definition_here · Uses: G1, S01

Leaf basis: definition_here

Complement each open relative to X to obtain all closed sets.



S03 · definitionBefore

F\supseteq A,\quad F\in\mathcal F

After

\overline A=X\cap\{b,c\}=\{b,c\}

Conditions: none

Rule: definition_here · Uses: G1, S02

Leaf basis: definition_here

The closed sets containing b are exactly X and {b,c}.



S04 · definitionBefore

U\subseteq A,\quad U\in\tau

After

A^\circ=\bigcup\{\varnothing\}=\varnothing

Conditions: none

Rule: definition_here · Uses: G1, S01

Leaf basis: definition_here

All nonempty opens contain a, so no nonempty open lies inside A.



S05 · definitionBefore

\partial A=\overline A\setminus A^\circ

After

\partial A=\{b,c\}

Conditions: none

Rule: definition_here · Uses: S03, S04

Leaf basis: definition_here

Apply the closure-minus-interior definition directly.



S06 · definitionBefore

D=\{a,c\}

After

\overline D=X,\quad D^\circ=\{a\}

Conditions: none

Rule: definition_here · Uses: G1, S01, S02

Leaf basis: definition_here

X is the only closed set containing a,c; empty and {a} are exactly the opens contained in D.



S07 · impliesBefore

\partial D=\overline D\setminus D^\circ

After

\partial D=\{b,c\}=\partial A=\overline A\cap\overline D

Conditions: none

Rule: sets · Uses: S05, S06

Leaf basis: sets

The complement boundary and the intersection of the two closures give the same result.



S08 · impliesBefore

\overline\varnothing=\varnothing,\ \varnothing^\circ=\varnothing,\ \overline X=X=X^\circ

After

\partial\varnothing=\partial X=\varnothing

Conditions: none

Rule: sets · Uses: S01, S02

Leaf basis: sets

Empty and whole space have empty boundary; no undefined geometric outer edge is used.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S01, S02 — Each closure and interior follows directly from the listed families.
- S07 · premise_audit · S05, S06 — Check all three equalities elementwise, claiming this explicit instance only.
- S06 · premise_audit · G1, S01, S02 — Re-enumerate for D instead of guessing symmetry from a drawing.
- S05 · premise_audit · S03, S04 — The boundary need not lie in A: c is a boundary point outside A.
- S04 · premise_audit · G1, S01 — A itself has not been silently assumed open.
- S03 · premise_audit · G1, S02 — {c} and empty do not contain b; the enumeration is complete.
- S02 · premise_audit · G1, S01 — Complementing twice returns the corresponding original open.
- S01 · premise_audit · G1 — All four members are supplied, so the chain argument checks all axioms.





## Error controls and negative controls

Compute both sidesList all open subsets and closed supersets for A and its complement independently.

Keep the carrierDifferences and complements use the same X.


- The boundary must lie in A. → reject — c is on the boundary but not in A.
- The boundary of X is X. → reject — Closure and interior of X are both X, giving an empty difference.
- The result is determined by distances between the points. → reject — No metric is supplied; the result comes from the listed topology.





## Result and limitations

Both complementary sets have boundary {b,c}; empty and X have empty boundaries.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 21eba37c5fc910925cb200b0b393070d907805f2655a1be31714240ec9c5add6
- original source SHA-256: 21eba37c5fc910925cb200b0b393070d907805f2655a1be31714240ec9c5add6
- 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-topological-boundary-01.json)