# Continuous maps between topological spaces: deciding continuity by preimages in finite spaces and separating it from openness

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

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-continuity-01 · production-20261019-adopted-96



## Goal and scope

Let X={1,2,3} with τX={∅,{1},{1,2},X}, and Y={a,b} with τY={∅,{a},Y}. For three maps given by complete tables, f (1↦a, 2↦a, 3↦b), g (1↦a, 2↦b, 3↦a) and c (everything ↦b), decide continuity by the preimage condition and decide whether each is an open map; prove that a composite of continuous maps is continuous and check it with q:Y→Z; finally count all continuous maps X→Y.

Works inside the MKO's scope: both underlying sets and topologies are fixed (assumption a1), maps are given by complete total tables, and a preimage collects every source element mapping into the target subset (assumption a2). The concrete map classification and count use the stated finite topologies; the general composition-continuity theorem is proved for arbitrary topological spaces without finiteness; the ε-δ continuity of real functions, subspaces and the isolated-point bridge are not, and the canonical MKO and its English edition are not changed.





## Givens and symbols


- image_preimage_def
- function_def
- composition_def
- set_builder
- subset_def


- G1 — Source space: X={1,2,3}, τX={∅,{1},{1,2},X} (MKO assumption a1).
- G2 — Target space: Y={a,b}, τY={∅,{a},Y} (MKO assumption a1).
- G3 — Maps given by complete total tables (MKO assumption a2): f(1)=a, f(2)=a, f(3)=b; g(1)=a, g(2)=b, g(3)=a; c(1)=c(2)=c(3)=b.
- G4 — A third space Z={0,1} with τZ={∅,{0},Z}, and the map q:Y→Z with q(a)=0, q(b)=1.


- (X,\tau_X) — the source space X={1,2,3}
- (Y,\tau_Y) — the target space Y={a,b}
- h^{-1}[V] — the preimage of V under h, {x∈X ∣ h(x)∈V}
- h[U] — the image of U under h, {h(x) ∣ x∈U}
- f,g,c — the three maps to be classified
- q:Y\to Z — the second map used to check composition





## Rules and sources


- image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- composition_def · prerequisite — Composition: for f:A→B and g:B→C, g∘f:A→C is defined by (g∘f)(a)=g(f(a)).
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- topology_def · prerequisite — Topology: a family τ of open subsets of X containing ∅ and X, closed under arbitrary unions and finite intersections.
- nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- mko_topological_continuity_def · cited — For topological spaces (X,τX), (Y,τY) and a total map f:X→Y, f is continuous exactly when f⁻¹[V]∈τX for every V∈τY. This is a preimage condition; it does not require images of open sets to be open. · mko-topological-continuity
- mko_topological_space_def · cited — A topology on X is a family τ⊆P(X) with ∅∈τ, X∈τ, unions of all subfamilies in τ and intersections of all finite subfamilies in τ (the empty union is ∅ and the empty intersection is X). · mko-topological-space
- open_map_def · prerequisite — A map h:X→Y is an open map if h[U]∈τY for every U∈τX.
- finite_exhaustion · prerequisite — For an explicitly listed finite set D, ∀V∈D, Q(V) is equivalent to the conjunction of Q over the listed elements; checking only some elements does not prove it, and one failing element refutes it.
- L_chain · lemma — If a finite family of subsets of a set S contains ∅ and S and any two members are comparable under ⊆ (a chain), then it is a topology on S.
- L_trivial_preimage · lemma — For every total map h:X→Y, h⁻¹[∅]=∅ and h⁻¹[Y]=X.
- L_comp_preimage · lemma — For h:X→Y, k:Y→Z and W⊆Z, (k∘h)⁻¹[W]=h⁻¹[k⁻¹[W]].





## Main derivation

S01 · theorem_applicationBefore

\tau_X,\ \tau_Y,\ \tau_Z

After

\text{each is a topology on}\ X,\ Y,\ Z

Conditions: \varnothing\subseteq\{1\}\subseteq\{1,2\}\subseteq X; \varnothing\subseteq\{a\}\subseteq Y; \varnothing\subseteq\{0\}\subseteq Z

Rule: L_chain · Uses: G1, G2, G4

Leaf basis: topology_def + subset_def

All three families are finite, contain the empty set and the whole set, and their members form an inclusion chain: ∅⊆{1}⊆{1,2}⊆X, ∅⊆{a}⊆Y, ∅⊆{0}⊆Z. By Lemma L_chain (proved in S01.1) all three are topologies. The definition of continuity needs topological spaces at both ends, so this is checked first.



S02 · equivalentBefore

h:X\to Y\ \text{continuous}

After

h^{-1}[\varnothing]\in\tau_X\ \wedge\ h^{-1}[\{a\}]\in\tau_X\ \wedge\ h^{-1}[Y]\in\tau_X

Conditions: \tau_Y=\{\varnothing,\{a\},Y\}

Rule: finite_exhaustion · Uses: S01, G2, mko_topological_continuity_def

Leaf basis: def_unfold + finite_exhaustion

Unfold the MKO definition: h is continuous exactly when h⁻¹[V]∈τX for every V∈τY. τY has only three members, so the universal condition is equivalent to the conjunction of three membership conditions. Deciding continuity requires checking every open set of the target, not a sample.



S03 · equivalentBefore

h^{-1}[\varnothing]\in\tau_X\wedge h^{-1}[\{a\}]\in\tau_X\wedge h^{-1}[Y]\in\tau_X

After

h\ \text{continuous}\iff h^{-1}[\{a\}]\in\tau_X

Conditions: h\ \text{total}

Rule: L_trivial_preimage · Uses: S02, G1

Leaf basis: and_intro_elim + image_preimage_def + topology_def

By Lemma L_trivial_preimage (proved in S03.1), every total map has h⁻¹[∅]=∅∈τX and h⁻¹[Y]=X∈τX, so these two conditions hold automatically. The only informative one is V={a}: h is continuous exactly when h⁻¹[{a}]∈τX. This also explains why checking only ∅ or Y can never detect discontinuity.



S04 · impliesBefore

f^{-1}[\{a\}]=\{x\in X\mid f(x)=a\}

After

f^{-1}[\{a\}]=\{1,2\}

Conditions: none

Rule: image_preimage_def · Uses: G3

Leaf basis: image_preimage_def + set_builder

Scan every row of f's complete table: f(1)=a is collected, f(2)=a is collected, f(3)=b is not. The preimage must collect every source element mapping to a, not just one.



S05 · impliesBefore

f^{-1}[\{a\}]=\{1,2\}

After

\{1,2\}\in\tau_X\ \Rightarrow\ f\ \text{continuous};\quad f\ \text{is an open map}

Conditions: none

Rule: mko_topological_continuity_def · Uses: S03, S04, G1, G3, open_map_def

Leaf basis: mko_topological_continuity_def + and_intro_elim + open_map_def

{1,2} is a member of τX, so by the equivalence of S03, f is continuous. The preimages of the three open sets are ∅, {1,2} and X, all in τX. Also take images of all four source open sets: f[∅]=∅, f[{1}]={a}, f[{1,2}]={a}, and f[X]=Y. All four images belong to τY, so f is also an open map by definition.



S06 · impliesBefore

g^{-1}[\{a\}]=\{x\in X\mid g(x)=a\}

After

g^{-1}[\{a\}]=\{1,3\}

Conditions: none

Rule: image_preimage_def · Uses: G3

Leaf basis: image_preimage_def + set_builder

Scan g's table: g(1)=a collected, g(2)=b not, g(3)=a collected, giving {1,3}.



S07 · impliesBefore

g^{-1}[\{a\}]=\{1,3\}

After

\{1,3\}\notin\tau_X\ \Rightarrow\ g\ \text{not continuous}

Conditions: none

Rule: quantifier_negation · Uses: S03, S06, G1

Leaf basis: quantifier_negation + finite_exhaustion

{1,3} equals none of the four members of τX, so it is not open. The open set {a} has a non-open preimage, so by quantifier negation 'every V∈τY has an open preimage' fails, and g is not continuous.



S08 · impliesBefore

g[U]\ \text{for}\ U\in\tau_X

After

g[\varnothing]=\varnothing,\ g[\{1\}]=\{a\},\ g[\{1,2\}]=Y,\ g[X]=Y\ \in\tau_Y

Conditions: none

Rule: open_map_def · Uses: G1, G2, G3

Leaf basis: open_map_def + image_preimage_def + finite_exhaustion

Compute the image under g of every open set of the source: the image of ∅ is ∅; of {1} is {a}; of {1,2} is {a,b}=Y; of X is {a,b}=Y. All four images are in τY, so g is an open map. But S07 showed g is not continuous: open sets having open images is not continuity (MKO paragraph 3).



S09 · impliesBefore

c^{-1}[\{a\}]=\{x\mid c(x)=a\}

After

c^{-1}[\{a\}]=\varnothing\in\tau_X\ \Rightarrow\ c\ \text{continuous}

Conditions: none

Rule: mko_topological_continuity_def · Uses: S03, G3, G1

Leaf basis: image_preimage_def + mko_topological_continuity_def

c sends every point to b and no point to a, so c⁻¹[{a}]=∅∈τX. By S03, c is continuous. A preimage does not need c to have an inverse: c is not injective, yet c⁻¹[{a}] is a well-defined set.



S10 · impliesBefore

c[X]

After

c[X]=\{b\}\notin\tau_Y\ \Rightarrow\ c\ \text{not open}

Conditions: none

Rule: quantifier_negation · Uses: G1, G2, G3

Leaf basis: quantifier_negation + open_map_def + image_preimage_def

X is open, and its image c[X]={b} is not in τY={∅,{a},Y}, so c is not an open map. c is continuous but not open; together with g from S07 and S08, neither of continuity and openness implies the other.



S11 · theorem_applicationBefore

h:X\to Y,\ k:Y\to Z\ \text{continuous},\ W\in\tau_Z

After

(k\circ h)^{-1}[W]=h^{-1}[k^{-1}[W]]\in\tau_X\ \Rightarrow\ k\circ h\ \text{continuous}

Conditions: none

Rule: L_comp_preimage · Uses: mko_topological_continuity_def

Leaf basis: composition_def + image_preimage_def + forall_intro

Let h and k be continuous and W∈τZ. By Lemma L_comp_preimage (proved in S11.1), (k∘h)⁻¹[W]=h⁻¹[k⁻¹[W]]. Continuity of k gives k⁻¹[W]∈τY, and continuity of h then gives h⁻¹[k⁻¹[W]]∈τX. W was an arbitrary open set, so k∘h is continuous. This holds for all topological spaces, not only finite ones.



S12 · impliesBefore

q^{-1}[\{0\}]=\{a\}\in\tau_Y,\ f\ \text{continuous}

After

(q\circ f)^{-1}[\{0\}]=f^{-1}[\{a\}]=\{1,2\}\in\tau_X

Conditions: none

Rule: forall_elim · Uses: S11, S05, G4, G3

Leaf basis: forall_elim + composition_def + image_preimage_def

q is continuous: q⁻¹[{0}]={a}∈τY, and the other two preimages are open automatically by L_trivial_preimage. By S11, q∘f is continuous, and (q∘f)⁻¹[{0}]=f⁻¹[q⁻¹[{0}]]=f⁻¹[{a}]={1,2}. Recomputing directly: q∘f sends 1 and 2 to 0 and 3 to 1, so (q∘f)⁻¹[{0}]={1,2}∈τX. The two computations agree.



S13 · impliesBefore

h\mapsto A_h=h^{-1}[\{a\}]\ \text{for}\ h:X\to Y

After

\#\{h:X\to Y\}=2^3=8,\ \#\{h\ \text{continuous}\}=|\tau_X|=4

Conditions: none

Rule: injective_surjective_def · Uses: S03, G1

Leaf basis: injective_surjective_def + finite_counting_basics + numeric_evaluation

Each map h:X→Y is determined by the set A_h=h⁻¹[{a}] (h(x)=a when x∈A_h and h(x)=b otherwise), and every subset A⊆X gives a map, so h↦A_h is a bijection between maps and subsets, giving 2^3=8 maps. By S03, h is continuous exactly when A_h∈τX, so there are exactly |τX|=4 continuous maps: A=∅ (that is c), A={1}, A={1,2} (that is f), A=X (constant a). g corresponds to A={1,3}, which is not among them.







## Substeps and lemmas

S01.1 · impliesBefore

\mathcal{F}\ \text{a finite chain},\ \varnothing,S\in\mathcal{F},\ F\subseteq\mathcal{F}

After

\textstyle\bigcup F\in\mathcal{F},\ \bigcap F\in\mathcal{F}

Conditions: none

Rule: nat_induction · Uses: nat_induction, set_operations_def, subset_def

Leaf basis: nat_induction + set_operations_def + subset_def

The family is finite, so every subfamily F is finite. If F is empty, ∪F=∅ and ∩F=S are in the family. If F is nonempty, induction on the number of members shows a finite chain has a largest member M and a smallest member m (a newly added member is comparable with the old largest and smallest). Every member is contained in M and contains m, so ∪F=M and ∩F=m, both in the family. Hence the family is closed under unions and intersections of every subfamily and is a topology, proving L_chain.



S03.1 · impliesBefore

x\in h^{-1}[\varnothing],\ x\in h^{-1}[Y]

After

h^{-1}[\varnothing]=\varnothing,\ h^{-1}[Y]=X

Conditions: h\ \text{total}

Rule: image_preimage_def · Uses: image_preimage_def, function_def

Leaf basis: image_preimage_def + function_def + set_extensionality

x∈h⁻¹[∅] means h(x)∈∅, which holds for no x, so h⁻¹[∅]=∅. x∈h⁻¹[Y] means h(x)∈Y; since h is total, every x∈X has h(x)∈Y, so h⁻¹[Y]=X. This proves L_trivial_preimage.



S11.1 · equivalentBefore

x\in(k\circ h)^{-1}[W]

After

x\in h^{-1}[k^{-1}[W]]

Conditions: none

Rule: image_preimage_def · Uses: composition_def, image_preimage_def

Leaf basis: composition_def + image_preimage_def + set_extensionality

x∈(k∘h)⁻¹[W] ⇔ (k∘h)(x)∈W ⇔ k(h(x))∈W ⇔ h(x)∈k⁻¹[W] ⇔ x∈h⁻¹[k⁻¹[W]]. Each move unfolds a definition, so by extensionality the two sets are equal, proving L_comp_preimage.







## Reverse audits


- S13 · premise_audit · S03, injective_surjective_def, finite_counting_basics — The count rests on the bijection and the equivalence of S03; it is a complete enumeration, not a sample (N1, N2, N3).
- S12 · premise_audit · S11, S05, G4, L_trivial_preimage — This is one instance of the general result with a direct recomputation; one instance cannot prove the general result in reverse.
- S11.1 · inverse_equivalence · composition_def, image_preimage_def, set_extensionality — Each move is an equivalent rewriting by definition, valid both ways. Note the order: first k, then h, the reverse of the composition order.
- S11 · premise_audit · L_comp_preimage, mko_topological_continuity_def, forall_intro — It needs both maps to be continuous; the converse (k∘h continuous implies h or k continuous) is not claimed.
- S10 · premise_audit · G2, open_map_def, quantifier_negation — One source open set with a non-open image suffices to refute openness.
- S09 · premise_audit · S03, G3, image_preimage_def — Preimage notation does not presuppose an inverse (image_preimage_def); the conclusion needs only ∅∈τX.
- S08 · premise_audit · G3, open_map_def, image_preimage_def — Being an open map is also a universal condition over all source open sets, and all four are checked. This step claims no implication between openness and continuity.
- S07 · premise_audit · S06, G1, quantifier_negation, finite_exhaustion — One counterexample V={a} suffices to refute the universal condition; deciding {1,3}∉τX requires comparing with each of the four members.
- S06 · premise_audit · G3, image_preimage_def — All three rows are checked.
- S05 · sufficient_goal_reduction · S03, S04, G1, G3, open_map_def — Goal: f is continuous. By S03 the necessary and sufficient condition is f⁻¹[{a}]∈τX, obtained forwards from S04 and the list of τX. The open-map part is separately established from the complete table G3 by checking images of all four source open sets, using open_map_def.
- S04 · premise_audit · G3, image_preimage_def, set_builder — All three rows of the complete table must be checked; missing a row could give a wrong preimage.
- S03.1 · premise_audit · image_preimage_def, function_def — The second equality needs h to be total; if some x had no value, h⁻¹[Y] would be smaller than X.
- S03 · inverse_equivalence · L_trivial_preimage, mko_topological_space_def — Dropping two always-true conjuncts does not change truth, so both directions hold; it needs ∅, X∈τX.
- S02 · inverse_equivalence · mko_topological_continuity_def, finite_exhaustion — A finite universal statement and the conjunction are equivalent both ways. The condition is about preimages lying in τX, not images lying in τY.
- S01.1 · premise_audit · nat_induction, set_operations_def, subset_def, mko_topological_space_def — It needs finiteness (so that largest and smallest members exist) and comparability; without either the conclusion can fail.
- S01 · premise_audit · G1, G2, G4, L_chain — It needs the complete lists of the three families and the chain condition; not every finite family is a topology, and being a chain is only a sufficient condition.





## Error controls and negative controls

Sending open sets to open sets is not the definition of continuityThe misconception identified in the MKO is taking 'images of open sets are open' as the definition of continuity. g maps every open set to an open set yet is not continuous (S07, S08); c is continuous yet maps the open set X to the non-open set {b} (S09, S10). Continuity is about preimages only.

Checking one open set is not enoughThe preimages of ∅ and Y are open for every total map (S03), so checking only them always 'passes'; that is exactly what happens for g. Every member of τY must be checked, and the decisive one is {a}.

Preimages do not need an inversec is not injective and has no inverse, yet c⁻¹[{a}]=∅ and c⁻¹[{b}]=X are well-defined sets. Reading f⁻¹ as an inverse function would wrongly suggest that continuity of non-injective maps cannot be decided.


- g maps every open set to an open set, so g is continuous → reject — g⁻¹[{a}]={1,3}∉τX.
- g⁻¹[∅]=∅ and g⁻¹[Y]=X are open, so g is continuous → reject — These two preimages are open for every total map; {a} must be checked, and g⁻¹[{a}]={1,3} is not open.
- c is continuous, so c maps open sets to open sets → reject — c[X]={b}∉τY.
- c is not injective, so c⁻¹ does not exist and the continuity of c cannot be decided → reject — Preimages do not need an inverse: c⁻¹[{a}]=∅∈τX, so c is continuous.





## Result and limitations

f is continuous and an open map (the images of all source open sets are ∅, {a}, {a}, Y; f⁻¹[{a}]={1,2}∈τX); g is not continuous (g⁻¹[{a}]={1,3}∉τX), yet g is an open map; c is continuous (c⁻¹[{a}]=∅) but not an open map (c[X]={b}∉τY). Composites of continuous maps are continuous, with q∘f as an example. Of the 8 maps X→Y, exactly 4 are continuous.


- The bridge to Mathlib's Continuous (open-preimage definition), to ε-δ continuity of real functions, and to subspaces and isolated points (MKO formal next) is not built here.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b117526fa854e48680a3b666c42aa17e7e65e805f5d983e78d1584911010c82d
- original source SHA-256: 6d48e6785097f15248cf83e69efa2ae7a0fd26ea5e6dd4144f0d3eb785992398
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-topological-continuity-01.json)