# Compactness of a finite subspace [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-compact-subset/) 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-compact-subset-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Prove K={b,c} compact in its ambient space and audit a relative-open cover. A complete finite model, without a universal closed-and-bounded substitution. ## Givens and symbols - sets - topology - definition_here - G1 — X={a,b,c}, tau={empty,{a},{a,b},X}, K={b,c}. - \tau_K — induced topology - V_i — relative-open cover member ## Rules and sources - mko_definition · cited — A cover must cover K, and a subcover must be selected from the original cover. Passing one cover audit does not prove general compactness. For the complete finite topology and finite subset used here, finiteness supplies compactness, including the empty subset by convention. Do not extrapolate this finite enumeration to infinite spaces or identify compactness with ambient closedness and boundedness without extra hypotheses. · mko-compact-subset - 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 — Relative opens of K are U intersect K for ambient-open U; K is compact when every relative-open cover has a finite subcover from its original indices. ## 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 The finite chain with both endpoints is closed under unions and intersections. S02 · definitionBefore U\cap K\ (U\in\tau) After \varnothing,\varnothing,\{b\},K Conditions: none Rule: definition_here · Uses: G1, S01 Leaf basis: definition_here Intersect each ambient open, retaining all four source entries. S03 · impliesBefore \tau_K=\{\varnothing,\{b\},K\} After \tau_K\text{ is a topology on }K Conditions: none Rule: topology · Uses: S02 Leaf basis: topology After deduplication this remains a finite chain containing empty and K. S04 · impliesBefore K\subseteq\bigcup_{i\in I}V_i,\quad V_i\in\tau_K After c\in V_j\text{ for some }j\in I Conditions: none Rule: sets · Uses: S03 Leaf basis: sets For an arbitrary relative-open cover, c belongs to an original member. S05 · impliesBefore c\in V_j\in\tau_K After V_j=K Conditions: none Rule: sets · Uses: S03, S04 Leaf basis: sets Only K in the complete relative family contains c. S06 · definitionBefore J=\{j\}\subseteq I,\quad\bigcup_{i\in J}V_i=K After K\text{ is compact in the subspace topology} Conditions: none Rule: definition_here · Uses: S04, S05 Leaf basis: definition_here Every relative-open cover has a one-member original subcover, establishing the universal definition. S07 · impliesBefore (V_1,V_2)=(\{b\},K) After J=\{2\}\text{ covers }K;\quad\{1\}\text{ does not} Conditions: none Rule: sets · Uses: G1, S03 Leaf basis: sets The supplied cover admits index {2}; choosing only {b} misses c. S08 · impliesBefore K=\varnothing\text{ as a separate boundary} After \varnothing\text{ has the empty finite subcover} Conditions: none Rule: sets · Uses: S03 Leaf basis: sets The empty subset is compact using the empty finite subcover, without inventing a member. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · S03 — Coverage of the empty target is vacuous, unlike the nonempty example. - S07 · premise_audit · G1, S03 — This instance is separate from the universal proof. - S06 · premise_audit · S04, S05 — This does not depend on whether K is ambient open or closed. - S05 · premise_audit · S03, S04 — The inference uses all three relative opens. - S04 · premise_audit · S03 — j depends on the cover; the cover is not a single fixed test. - S03 · premise_audit · S02 — The universe at this step is K. - S02 · premise_audit · G1, S01 — Ambient witnesses need not be subsets of K. - S01 · premise_audit · G1 — The full four-member family is checked. ## Error controls and negative controls Cover KThe relative union must contain K, not X. Original indicesA finite subcover retains original-family members. - {b} alone covers K. → reject — c is missing. - Every relative open is ambient open. → reject — {b} is not in the ambient topology. - Compact always means closed and bounded in any topology. → reject — No metric is supplied, and the general equivalence needs additional premises. ## Result and limitations K is compact in the induced topology, whose opens are empty, {b} and K. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 56c43748460b659d5e4882ad8b91e59c79a448b72613dbffe32f07c5de2c09e5 - original source SHA-256: 56c43748460b659d5e4882ad8b91e59c79a448b72613dbffe32f07c5de2c09e5 - 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-compact-subset-01.json)