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

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

\tau_X,\ \tau_Y,\ \tau_Z

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

c[X]

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

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

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

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

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

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

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

Substeps and lemmas

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

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

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

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

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

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

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 continuity

The 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 enough

The 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 inverse

c 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)