# Relative openness differs from ambient openness

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

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-subspace-topology-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Compute the subspace topology and all relative closed sets of Y={b,c}.

A complete finite ambient topology; relative complements are inside Y.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau_X={empty,{a},{a,b},X}, Y={b,c}.


- Y — subspace carrier
- \tau_Y — relative topology





## Rules and sources


- mko_definition · cited — The induced topology is {U∩Y:U∈tau_X}, normalizing duplicate and empty intersections. Relative opens need not be ambient open and their witnesses U need not lie inside Y. Relative closedness uses open complements inside Y, or intersections with ambient closed sets. Y is the relative universe in every topology obligation. · mko-subspace-topology
- 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 — The subspace topology consists of intersections of ambient opens with the subspace carrier; relative closed sets are complements of relative opens inside that carrier.





## Main derivation

S01 · impliesBefore

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

After

\tau_X\text{ is a topology},\quad Y\subseteq X

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

The parent is a complete finite chain with endpoints and union/intersection closure; Y is indeed a subset.



S02 · equivalentBefore

\varnothing\cap Y,\ \{a\}\cap Y

After

\varnothing,\ \varnothing

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

The first two ambient opens have empty intersections; keep the duplicate until normalization.



S03 · equivalentBefore

\{a,b\}\cap Y,\ X\cap Y

After

\{b\},\ Y

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

The remaining intersections give {b} and the relative whole space Y.



S04 · definitionBefore

\tau_Y=\{U\cap Y:U\in\tau_X\}

After

\tau_Y=\{\varnothing,\{b\},Y\}

Conditions: none

Rule: definition_here · Uses: S02, S03

Leaf basis: definition_here

After deduplication, list every relative open.



S05 · impliesBefore

\varnothing\subset\{b\}\subset Y

After

\tau_Y\text{ is a topology on }Y

Conditions: none

Rule: topology · Uses: S04

Leaf basis: topology

With Y as the universe, verify the finite chain's union/intersection axioms.



S06 · definitionBefore

\{Y\setminus V:V\in\tau_Y\}

After

\mathcal F_Y=\{Y,\{c\},\varnothing\}

Conditions: none

Rule: definition_here · Uses: S04

Leaf basis: definition_here

Complement within Y to obtain all relative closed sets.



S07 · impliesBefore

\{b\}\in\tau_Y

After

\{b\}\notin\tau_X

Conditions: none

Rule: sets · Uses: G1, S04

Leaf basis: sets

{b} is relatively open but not ambient open; these are distinct predicates.



S08 · impliesBefore

Y\setminus\{c\}=\{b\}\in\tau_Y

After

\{c\}\text{ is relatively closed};\quad\{b\}\text{ is not relatively closed}

Conditions: none

Rule: sets · Uses: S06, S07

Leaf basis: sets

The complement of {c} is relatively open; the complement {c} of {b} is not relatively open.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S06, S07 — Relative closedness is checked against the entire relative topology.
- S07 · premise_audit · G1, S04 — The ambient-open witness is {a,b}, not {b} itself.
- S06 · premise_audit · S04 — Complementing in X instead could produce sets not contained in Y.
- S05 · premise_audit · S04 — The whole-space member is Y, not X.
- S04 · premise_audit · S02, S03 — All four ambient opens were intersected, so no relative open is missing.
- S03 · inverse_equivalence · G1 — The witnessing ambient open {a,b} need not lie inside Y.
- S02 · inverse_equivalence · G1 — An empty intersection is still a legal relative open.
- S01 · premise_audit · G1 — Parent validity is not inferred circularly from the desired subspace family.





## Error controls and negative controls

List every intersectionTraverse every ambient open before deduplicating.

Relative universeRelative complements and axioms consistently use Y.


- The witnessing ambient open must lie inside Y. → reject — The witness {a,b} for {b} is not contained in Y.
- {b} is open in X. → reject — It is absent from the complete ambient topology.
- The relative whole space is still X. → reject — The relative topology has whole space Y.





## Result and limitations

tau_Y={empty,{b},Y}; the relative closed sets are {empty,{c},Y}.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 24419aa4e704355f75ed3b708e05ec2f2252aa18cea0d39bb65e43fd886167b6
- original source SHA-256: 24419aa4e704355f75ed3b708e05ec2f2252aa18cea0d39bb65e43fd886167b6
- 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-subspace-topology-01.json)