# Pull back covers and return the same indices

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-continuous-image-of-compact/)

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-continuous-image-of-compact-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Demonstrate the compact-image cover proof with an explicit finite map.

Complete finite topologies with an arbitrary-cover pullback argument; no converse.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b}, tau_X={empty,{a},{b},X}; Y={u,v}, tau_Y={empty,{u},Y}; K=X.
- G2 — f(a)=f(b)=u.


- W_i — target-open cover of the image
- J — retained original indices





## Rules and sources


- mko_definition · cited — Pull an ambient-open cover of f(K) back along f. Continuity makes preimages open and they cover K. A finite subcover of K pushes forward using the same cover indices to cover f(K). Injectivity and surjectivity are not required. Compactness of an image does not imply compactness of the domain. Compact preimages and closed images require additional hypotheses, often Hausdorff for closedness. · mko-continuous-image-of-compact
- 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 — Continuity requires every target-open preimage to be open; relative opens intersect ambient opens with the subspace; compactness requires a finite original-index subcover of every relative-open cover; closed sets have open complements.





## Main derivation

S01 · impliesBefore

\tau_X=\mathcal P(X),\quad\varnothing\subset\{u\}\subset Y

After

\tau_X,\tau_Y\text{ are topologies}

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

The source is the power set and the target a finite chain with endpoints; both satisfy every axiom.



S02 · impliesBefore

f^{-1}(\varnothing),f^{-1}(\{u\}),f^{-1}(Y)

After

\varnothing,X,X\in\tau_X

Conditions: none

Rule: definition_here · Uses: G1, G2, S01, definition_here

Leaf basis: definition_here

Check preimages of all target opens, proving continuity of f.



S03 · impliesBefore

K=X=\{a,b\}

After

K\text{ is compact}

Conditions: none

Rule: definition_here · Uses: G1, definition_here

Leaf basis: definition_here

From any cover choose one original member for a and one for b; at most two cover K.



S04 · impliesBefore

f(K)=\{u\}\subseteq\bigcup_{i\in I}W_i,\quad W_i\in\tau_Y

After

K\subseteq\bigcup_{i\in I}(K\cap f^{-1}(W_i))

Conditions: none

Rule: sets · Uses: G2, S02

Leaf basis: sets

Take an arbitrary ambient-open cover of the image; each x in K has its image in some W_i, so the preimages cover K.



S05 · impliesBefore

W_i\in\tau_Y

After

K\cap f^{-1}(W_i)\text{ is relatively open in }K

Conditions: none

Rule: definition_here · Uses: S02, S04, definition_here

Leaf basis: definition_here

Continuity gives an ambient-open preimage; intersection with K is relatively open.



S06 · theorem_applicationBefore

K\subseteq\bigcup_{i\in I}(K\cap f^{-1}(W_i))

After

K\subseteq\bigcup_{i\in J}f^{-1}(W_i),\quad J\subseteq I\text{ finite}

Conditions: none

Rule: definition_here · Uses: S03, S04, S05, definition_here

Leaf basis: definition_here

Compactness of K supplies a finite subset J of original indices.



S07 · impliesBefore

z\in f(K),\ z=f(x),\ x\in K

After

z\in\bigcup_{i\in J}W_i

Conditions: none

Rule: sets · Uses: S06

Leaf basis: sets

Some selected preimage contains x, so the same W_i contains z; return exactly the same indices.



S08 · impliesBefore

\forall(W_i)\text{ covering }f(K),\ \exists J\text{ finite covering }f(K)

After

f(K)=\{u\}\text{ is compact but not closed in }Y

Conditions: none

Rule: definition_here · Uses: S04, S07, definition_here

Leaf basis: definition_here

The first part proves compactness; {u} is not closed because {v} is not open, protecting the missing-Hausdorff boundary.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S04, S07, definition_here — Compactness and closedness are determined by separate obligations.
- S07 · premise_audit · S06 — No false equality between the image of a preimage and W_i is used; inclusion suffices.
- S06 · premise_audit · S03, S04, S05, definition_here — Finiteness of J comes from compactness, not an assumption that I is finite.
- S05 · premise_audit · S02, S04, definition_here — Coverage cannot substitute for the openness premise.
- S04 · premise_audit · G2, S02 — Only image membership is used, not surjectivity onto Y.
- S03 · premise_audit · G1, definition_here — The finite selection applies to every cover, not just one successful instance.
- S02 · premise_audit · G1, G2, S01, definition_here — Neither injectivity nor surjectivity is required, and neither holds here.
- S01 · premise_audit · G1 — No target open has been omitted.





## Error controls and negative controls

Preimages, not open imagesPull the cover back by continuity's preimage condition.

Preserve indicesJ is taken from and returned to the original target cover.


- The theorem requires f injective. → reject — Both points have the same image here and compactness still follows.
- A compact image forces a compact domain. → reject — The constant map (0,1) to {u} has compact image; the cover (1/n,1), n≥2, has no finite subcover of the domain.
- Every continuous compact image is closed. → reject — The complement {v} of {u} is not open here.





## Result and limitations

The continuous image {u} is compact but not closed in this non-Hausdorff target.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: d6eaece8c24bc185ce8421028d38a700da364006b5f47dd2476ede583c0cbbbc
- original source SHA-256: d6eaece8c24bc185ce8421028d38a700da364006b5f47dd2476ede583c0cbbbc
- 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-continuous-image-of-compact-01.json)