# A finite-chain basis and every generated open

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

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



## Goal and scope

Verify B={{a},{a,b},X} is a basis for the specified topology.

Complete finite basis and topology, distinct from a subbasis.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, B={{a},{a,b},X}; target tau={empty,{a},{a,b},X}.


- \mathcal B — candidate basis
- \mathcal T_{\mathcal B} — all basis unions





## Rules and sources


- mko_definition · cited — Every basis element is a subset of X and their union covers X. If x lies in B1∩B2, some B3 contains x and lies inside that intersection. A basis for an existing topology additionally consists of open sets and generates every open set as a union. A basis must not be confused with a subbasis. · mko-topological-basis
- 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 — A basis covers the carrier and locally refines every intersection point; its generated topology consists of all subfamily unions; for an existing topology its members must be open and generate all opens.





## Main derivation

S01 · impliesBefore

B\in\mathcal B

After

B\subseteq X\quad\text{for all three members}

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

Each of the three basis candidates lies in the same carrier.



S02 · impliesBefore

\bigcup\mathcal B=\{a\}\cup\{a,b\}\cup X

After

\bigcup\mathcal B=X

Conditions: none

Rule: sets · Uses: G1, S01

Leaf basis: sets

Because X itself belongs to the family, coverage holds.



S03 · impliesBefore

B_1,B_2\in\mathcal B

After

B_1\cap B_2=\min_{\subseteq}(B_1,B_2)\in\mathcal B

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

The three members form an inclusion chain; each of the six unordered pairs with repetition intersects to its smaller member.



S04 · impliesBefore

x\in B_1\cap B_2

After

B_3=B_1\cap B_2,\quad x\in B_3\subseteq B_1\cap B_2

Conditions: none

Rule: sets · Uses: S03

Leaf basis: sets

Use the intersection itself as the local refinement, since the previous step puts it in the basis.



S05 · definitionBefore

\mathcal T_{\mathcal B}=\{\bigcup\mathcal C:\mathcal C\subseteq\mathcal B\}

After

\mathcal T_{\mathcal B}=\{\varnothing,\{a\},\{a,b\},X\}

Conditions: none

Rule: definition_here · Uses: G1

Leaf basis: definition_here

The eight subfamilies have four distinct unions; the empty subfamily gives empty and every nonempty one gives its largest member.



S06 · impliesBefore

\mathcal T_{\mathcal B}\text{ is a finite inclusion chain with endpoints}

After

\mathcal T_{\mathcal B}\text{ is a topology}

Conditions: none

Rule: topology · Uses: S05

Leaf basis: topology

The chain verifies union and intersection closure of the complete four-member family.



S07 · definitionBefore

\mathcal B\subseteq\tau,\quad\mathcal T_{\mathcal B}=\tau

After

\mathcal B\text{ is a basis for the supplied }\tau

Conditions: none

Rule: definition_here · Uses: G1, S05

Leaf basis: definition_here

Every basis member is open and every target open is a basis union; both generation obligations hold.



S08 · impliesBefore

\mathcal C=\{\{a,b\},\{b,c\}\}

After

b\in\{a,b\}\cap\{b,c\},\quad\nexists C\in\mathcal C:\ b\in C\subseteq\{b\}

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

A family covering X may fail intersection refinement, demonstrating that coverage alone does not make a basis.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1 — The failed point b and both candidates are explicit, allowing exhaustive rejection.
- S07 · premise_audit · G1, S05 — Openness alone would be insufficient; S05 supplies generation of all opens.
- S06 · premise_audit · S05 — The target family was not merely assumed to be a topology; its axioms were checked.
- S05 · premise_audit · G1 — All unions were considered, not merely the basis members.
- S04 · premise_audit · S03 — This does not require arbitrary bases to be intersection-closed; this example permits that choice.
- S03 · premise_audit · G1 — The chain argument covers every pair without untested exceptions.
- S02 · premise_audit · G1, S01 — Coverage is only the first basis obligation; intersection refinement remains.
- S01 · premise_audit · G1 — No basis element may contain a point outside the carrier.





## Error controls and negative controls

Intersection-point quantifierEvery pair and every intersection point needs a refinement, not just coverage.

Two-way generationCheck basis openness and generation of every target open.


- Every cover is a basis. → reject — The two-set cover in S08 lacks a refinement at b.
- The generated topology need not contain empty. → reject — The empty union must be included.
- Open basis candidates alone prove generation of an existing topology. → reject — Every existing open must additionally be their union.





## Result and limitations

B is a basis of the supplied tau, generating exactly four opens.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 16ceb5eebc9f37a1b5a839cd909ba4c61c0319da66fca248b310dbd7dd5c0c8c
- original source SHA-256: 16ceb5eebc9f37a1b5a839cd909ba4c61c0319da66fca248b310dbd7dd5c0c8c
- 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-basis-01.json)