# Selecting a subcover by original indices

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

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-open-cover-and-subcover-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit a supplied open cover of K={a,b} and its subcover indices.

This audits one cover only, not universal compactness.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau is the entire power set of X; K={a,b}.
- G2 — The ordered family is U_1={a}, U_2={b}, U_3={a,b}, U_4={c}. Normalize the raw selection (3,3) to {3}.


- K — covered target
- U_i — original cover member
- I — normalized index set





## Rules and sources


- mko_definition · cited — Check openness of every supplied member, target inclusion in the union and the selection indices completely. A finite subcover for one supplied cover certifies that cover only; it is not by itself the universal compactness obligation. · mko-open-cover-and-subcover
- 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 — An open cover has open members whose union contains the target; a subcover uses a subset of the original indices and covers the same target.





## Main derivation

S01 · impliesBefore

\tau=\mathcal P(X)

After

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

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

List all eight subsets. Every union and finite intersection remains a subset of X, so this is a topology.



S02 · impliesBefore

i\in\{1,2,3,4\}

After

U_i\in\tau

Conditions: none

Rule: sets · Uses: G1, G2, S01

Leaf basis: sets

Each member occurs in the eight-open list; U_4 may be disjoint from K and still be legal.



S03 · impliesBefore

\bigcup_{i=1}^4 U_i

After

\{a\}\cup\{b\}\cup\{a,b\}\cup\{c\}=X

Conditions: none

Rule: sets · Uses: G2

Leaf basis: sets

The union of the supplied ordered family is X and therefore covers K.



S04 · impliesBefore

(3,3)

After

I=\{3\}\subseteq\{1,2,3,4\}

Conditions: none

Rule: sets · Uses: G2

Leaf basis: sets

Removing a duplicate index does not change the selected union.



S05 · equivalentBefore

\bigcup_{i\in I}U_i

After

U_3=\{a,b\}=K

Conditions: none

Rule: sets · Uses: G1, G2, S04

Leaf basis: sets

The third original set alone covers the target.



S06 · definitionBefore

I=\{3\},\quad K\subseteq\bigcup_{i\in I}U_i

After

(U_i)_{i\in I}\text{ is a finite open subcover}

Conditions: none

Rule: definition_here · Uses: S02, S04, S05

Leaf basis: definition_here

Openness is inherited from the original member, and a singleton index set is finite.



S07 · impliesBefore

J=\{1\}

After

\bigcup_{i\in J}U_i=\{a\}\not\supseteq K

Conditions: none

Rule: sets · Uses: G1, G2

Leaf basis: sets

A selection missing b is a negative check: a valid cover does not make every subfamily a cover.



S08 · impliesBefore

\exists I\text{ finite for this supplied cover}

After

\text{this supplied cover has a finite subcover}

Conditions: none

Rule: sets · Uses: S06

Leaf basis: sets

Conclude only for the audited cover; the universal statement over every open cover is a separate obligation.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S06 — No reversal from one successful selection to all covers has occurred.
- S07 · premise_audit · G1, G2 — The failure is missing b, not lack of openness of U_1.
- S06 · premise_audit · S02, S04, S05 — Openness, original-index membership and coverage are separate obligations supplied earlier.
- S05 · inverse_equivalence · G1, G2, S04 — Read the normalized index back from the original family instead of inventing a set from the target.
- S04 · premise_audit · G2 — Index 3 belongs to the original family; no new set has been introduced.
- S03 · premise_audit · G2 — Coverage requires inclusion of K, not equality with K.
- S02 · premise_audit · G1, G2, S01 — An open cover need not have every member inside K or make every member necessary.
- S01 · premise_audit · G1 — The four cover members are not being substituted for the complete topology.





## Error controls and negative controls

Index provenanceRead every selected member from the original ordered family.

No quantifier promotionSeparate one successful subcover from success for every open cover.


- Selecting {a,b,c} counts as a subcover of the original family. → reject — X is open but is not a member of the original family; a subcover cannot add it.
- {1} covers K. → reject — Its union misses b.
- This success proves all spaces compact. → reject — Only one supplied cover was checked, not the universal quantifier.





## Result and limitations

{3} indexes a valid finite subcover; {1} does not.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 5da7ac00e9a6cf40783fb48632b4b9388c717c3012a47aff481fcdd179f5f222
- original source SHA-256: 5da7ac00e9a6cf40783fb48632b4b9388c717c3012a47aff481fcdd179f5f222
- 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-open-cover-and-subcover-01.json)