# Closure and interior in a three-point chain topology

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

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-closure-and-interior-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Find the closure and interior of A={b}.

An exhaustive finite-topology calculation; no metric is supplied.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, the entire candidate family is tau={empty,{a},{a,b},X}, and A={b}.


- \tau — complete open family
- \overline A — closure
- A^\circ — interior





## Rules and sources


- mko_definition · cited — First validate the complete finite topology, then calculate closure and interior exactly from all closed supersets or open subsets. Retain the empty-set and whole-space boundaries and dependence on the topology; do not silently introduce a metric. · mko-closure-and-interior
- 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 are relative complements of opens; closure intersects all closed supersets and interior unites all open subsets.





## Main derivation

S01 · impliesBefore

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

After

\varnothing,X\in\tau

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

Every listed member is a subset of X, and both required endpoint sets are present.



S02 · impliesBefore

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

After

U\cup V=\max_{\subseteq}(U,V),\quad U\cap V=\min_{\subseteq}(U,V)

Conditions: none

Rule: sets · Uses: G1, S01

Leaf basis: sets

The family is a finite inclusion chain. For every nonempty subfamily, its union is its largest member and its intersection is its smallest member. The empty union is the empty set, and the empty intersection is X. All topology axioms follow.



S03 · definitionBefore

F=X\setminus U\ (U\in\tau)

After

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

Conditions: none

Rule: definition_here · Uses: G1, S02

Leaf basis: definition_here

Take each complement relative to X to obtain every closed set, including the empty set.



S04 · equivalentBefore

A=\{b\},\quad A\subseteq F\in\mathcal F

After

\{F\in\mathcal F:A\subseteq F\}=\{\{b,c\},X\}

Conditions: none

Rule: sets · Uses: G1, S03

Leaf basis: sets

Empty and {c} miss b; the other two closed sets are precisely the closed supersets.



S05 · definitionBefore

\overline A=\bigcap\{F\text{ closed}:A\subseteq F\}

After

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

Conditions: none

Rule: definition_here · Uses: S04

Leaf basis: definition_here

The closure is the intersection of all closed supersets, not an arbitrary selected superset.



S06 · equivalentBefore

U\in\tau,\quad U\subseteq\{b\}

After

\{U\in\tau:U\subseteq A\}=\{\varnothing\}

Conditions: none

Rule: sets · Uses: G1, S02

Leaf basis: sets

Every nonempty open set contains a, so none lies in {b}.



S07 · definitionBefore

A^\circ=\bigcup\{U\in\tau:U\subseteq A\}

After

A^\circ=\varnothing

Conditions: none

Rule: definition_here · Uses: S06

Leaf basis: definition_here

The interior unites all open subsets; the only such member is empty.



S08 · impliesBefore

A^\circ\subseteq A\subseteq\overline A

After

\varnothing\subseteq\{b\}\subseteq\{b,c\}

Conditions: none

Rule: sets · Uses: S05, S07

Leaf basis: sets

Substitute the results into both basic inclusions; a different topology can give different answers.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S05, S07 — The inclusions are consistency checks; the exhaustive intersection and union establish the actual constructions.
- S07 · premise_audit · S06 — Empty is open and contained in A, and no larger open subset was omitted.
- S06 · inverse_equivalence · G1, S02 — All three nonempty opens have been checked, rather than inferred from a label.
- S05 · premise_audit · S04 — The result is closed and contains A; every closed superset contains it, verifying minimality.
- S04 · inverse_equivalence · G1, S03 — Both selected sets contain b and both rejected sets do not; all four have been exhausted.
- S03 · premise_audit · G1, S02 — Complementing the four closed sets returns exactly the topology and checks the ambient carrier.
- S02 · premise_audit · G1, S01 — The chain argument covers the complete listed family, not one tested pair.
- S01 · premise_audit · G1 — Endpoint membership alone is insufficient; intersections and unions still need checking.





## Error controls and negative controls

Whole-family obligationList every closed superset before intersecting and every open subset before uniting.

Ambient bindingAll complements are relative to X, not A.


- The closure is X because X is closed and contains A. → reject — The smaller closed superset {b,c} was omitted.
- The interior of {b} is {b}. → reject — {b} is absent from the complete open family.
- These answers hold for every topology on X. → reject — In the discrete topology {b} itself is open and closed.





## Result and limitations

In this topology the closure is {b,c} and the interior is empty. Empty and X each equal their own closure and interior.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4d2edbe08895d69e94f4ee3bf38a0402fcb0ae2147791f8a665f438b55ac9303
- original source SHA-256: 2fa41873c0ddcc9253a540235a90fa71fd13d0554b298df20b082b0267e4e54a
- 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-closure-and-interior-01.json)