Topological space: fully verifying a chain of open sets on a three-point set, and recognising non-topologies

Goal and scope

Let X={a,b,c} with a, b, c distinct. (1) Prove that τ₁={∅,{a},{a,b},X} is a topology on X, covering all 16 subfamilies (including the empty one); (2) prove that τ₂={∅,{a},{b},X} is not a topology, and say which checks it does pass; (3) compare τ₁ with the indiscrete and discrete topologies; (4) on ℕ, prove that τ_fin={finite subsets of ℕ}∪{ℕ} is closed under pairwise unions and finite intersections but is not a topology.

Verifies each condition from the MKO's definition (with the empty-family convention a2). In the finite example a chain lemma handles all nonempty subfamilies at once, and a count confirms that all 16 subfamilies are covered, not sampled. The infinite example serves only to separate 'pairwise closure' from 'arbitrary closure'. Continuous maps, bases and metric topologies are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• subset_def
• set_operations_def
• set_extensionality
• nat_induction
• numeric_evaluation

• G1 — X={a,b,c} with a, b, c pairwise distinct; τ₁={∅,{a},{a,b},X}; τ₂={∅,{a},{b},X}.
• G2 — MKO assumption a2: arbitrary unions include the empty family and finite intersections include the empty family; the empty intersection is read as X.
• G3 — ℕ includes 0; τ_fin={A⊆ℕ : A finite}∪{ℕ}.

• X=\{a,b,c\} — the underlying set, with a, b, c distinct
• \tau_1,\ \tau_2 — two candidate families of subsets of X
• \mathcal{S}\subseteq\tau — a subfamily of τ
• \bigcup\mathcal{S},\ \bigcap\mathcal{S} — union and intersection of a subfamily (intersection relative to X)
• \mathcal{P}(X) — the power set, i.e. the discrete topology
• \tau_{\mathrm{fin}} — the candidate family on ℕ
• E — the set of even numbers in ℕ

Rules and sources

• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• 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₀.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• mko_topology_def · cited — For a set X, a topology on X is a family τ⊆P(X) such that ∅∈τ, X∈τ, the union of any subfamily of τ belongs to τ, and the intersection of any finite subfamily of τ belongs to τ. The pair (X,τ) is a topological space. · mko-topological-space
• family_ops · prerequisite — For a family 𝒮 of subsets of X: x∈⋃𝒮 ⇔ x∈A for some A∈𝒮; x∈⋂𝒮 ⇔ x∈X and x∈A for every A∈𝒮. Hence ⋃∅=∅ and ⋂∅=X.
• finite_sets · prerequisite — The union of two finite sets is finite; a subset of a finite set is finite; every finite nonempty subset of ℕ has a largest element.
• L_chain_extremes · lemma — If any two members of a finite nonempty family 𝒮 are comparable under ⊆, then 𝒮 has a largest member M (A⊆M for every A∈𝒮) and a smallest member m (m⊆A for every A∈𝒮).
• L_chain_union · lemma — If M∈𝒮 is the largest member of 𝒮 then ⋃𝒮=M; if m∈𝒮 is the smallest member then ⋂𝒮=m (members of 𝒮 being subsets of X).

Main derivation

\tau\ \text{is a topology on}\ X

\tau\subseteq\mathcal{P}(X),\ \varnothing,X\in\tau,\ \forall\mathcal{S}\subseteq\tau:\ \bigcup\mathcal{S}\in\tau,\ \forall\ \text{finite}\ \mathcal{S}\subseteq\tau:\ \bigcap\mathcal{S}\in\tau

\tau_1=\{\varnothing,\{a\},\{a,b\},X\}

\tau_1\subseteq\mathcal{P}(X)

\mathcal{S}=\varnothing\subseteq\tau_1

\bigcup\varnothing=\varnothing\in\tau_1,\quad \bigcap\varnothing=X\in\tau_1

\varnothing,\ \{a\},\ \{a,b\},\ X

\varnothing\subseteq\{a\}\subseteq\{a,b\}\subseteq X

\varnothing\neq\mathcal{S}\subseteq\tau_1

\mathcal{S}\ \text{has a largest member}\ M\ \text{and a smallest member}\ m

M,\ m\ \text{largest and smallest in}\ \mathcal{S}

\bigcup\mathcal{S}=M,\quad \bigcap\mathcal{S}=m

\mathcal{S}\subseteq\tau_1\ \text{arbitrary}

\bigcup\mathcal{S}\in\tau_1

\mathcal{S}\subseteq\tau_1\ \text{finite}

\bigcap\mathcal{S}\in\tau_1

\tau_1\subseteq\mathcal{P}(X),\ \text{unions and finite intersections closed}

(X,\tau_1)\ \text{is a topological space}

\{a\},\ \{b\}\in\tau_2

\{a\}\cup\{b\}=\{a,b\}\notin\tau_2

\tau_2=\{\varnothing,\{a\},\{b\},X\}

\varnothing,X\in\tau_2,\ \text{and}\ A\cap B\in\tau_2\ \text{for all}\ A,B\in\tau_2

\{\varnothing,X\},\ \tau_1,\ \mathcal{P}(X)

\{\varnothing,X\}\subsetneq\tau_1\subsetneq\mathcal{P}(X)

A,B\in\tau_{\mathrm{fin}}

A\cup B\in\tau_{\mathrm{fin}},\ A\cap B\in\tau_{\mathrm{fin}};\ \varnothing,\mathbb{N}\in\tau_{\mathrm{fin}}

\mathcal{S}=\{\{2k\}:k\in\mathbb{N}\}\subseteq\tau_{\mathrm{fin}}

\bigcup\mathcal{S}=E\notin\tau_{\mathrm{fin}}

\text{goals (1) to (4)}

\tau_1\ \text{topology};\ \tau_2,\ \tau_{\mathrm{fin}}\ \text{not topologies};\ \{\varnothing,X\}\subsetneq\tau_1\subsetneq\mathcal{P}(X)

Substeps and lemmas

|\mathcal{S}|=1,\ \mathcal{S}=\{A\}

M=m=A

|\mathcal{S}|=n+1,\ \mathcal{S}=\mathcal{S}'\cup\{A\},\ \mathcal{S}'\ \text{has}\ M',m'

\mathcal{S}\ \text{has a largest and a smallest member}

P(1)\ \land\ \forall n\ge 1\,(P(n)\Rightarrow P(n+1))

\forall n\ge 1:\ P(n)

M\in\mathcal{S},\ \forall A\in\mathcal{S}:\ A\subseteq M

\bigcup\mathcal{S}=M

m\in\mathcal{S},\ \forall A\in\mathcal{S}:\ m\subseteq A,\ m\subseteq X

\bigcap\mathcal{S}=m

1\in E\ ?

1\notin E,\ \text{so}\ E\neq\mathbb{N}

E\ \text{finite}\ ?

E\ \text{is infinite}

Reverse audits

• S15 · sufficient_goal_reduction · S09, S10, S12, S14, and_intro_elim — Goal G: the four parts. Sufficient condition H: the conclusions of S09, S10, S12 and S14; H⇒G is conjunction, and H is proved forwards from the givens.
• S14.2 · premise_audit · finite_sets, contradiction — The contradiction relies on 'a finite nonempty set of naturals has a largest element' and 2j+2=2(j+1) (N6).
• S14.1 · premise_audit · set_extensionality, order_basics — One natural number outside E suffices to show the sets differ (N5).
• S14 · premise_audit · G3, family_ops — The counterexample needs an infinite subfamily; unions of finite subfamilies cause no problem (S13). The conclusion depends on S14.1 and S14.2.
• S13 · premise_audit · G3, finite_sets, case_analysis — The cases are exhaustive; only pairwise (hence finite) closure is claimed, not closure under arbitrary unions.
• S12 · premise_audit · S09, subset_def, set_operations_def — Finer and coarser compare families of open sets by inclusion (MKO paragraph 2), not the size of the underlying set; each strict inclusion is confirmed by a witness member ({a} and {b}).
• S11 · premise_audit · G1, set_operations_def — This step does not change the conclusion of S10; it only shows which checks τ₂ passes.
• S10 · premise_audit · G1, set_operations_def, set_extensionality — One counterexample subfamily suffices to refute; it uses that a, b, c are pairwise distinct (G1).
• S09 · sufficient_goal_reduction · S02, S03, S07, S08, mko_topology_def, and_intro_elim — Goal G: τ₁ is a topology. Sufficient condition H: S02, S03, S07 and S08 together; H⇒G by the definition. H is proved forwards from G1 and G2; G is never used as a premise.
• S08 · premise_audit · S03, S05, S06, case_analysis — The two cases exhaust all finite subfamilies.
• S07 · premise_audit · S03, S05, S06, case_analysis — 'Empty' and 'nonempty' exhaust all subfamilies; since τ₁ is finite, every subfamily is finite, so no infinite subfamily is missed.
• S06.2 · premise_audit · family_ops, set_extensionality — It uses the fact that m is the smallest member and m⊆X; the lemma itself is not used.
• S06.1 · premise_audit · family_ops, set_extensionality — The two inclusions use M∈𝒮 and the fact that M is the largest member, respectively; the lemma itself is not used.
• S06 · premise_audit · S05, L_chain_union — M and m must belong to 𝒮; the empty family has no largest member, which is why it was handled separately in S03.
• S05.3 · premise_audit · S05.1, S05.2, nat_induction — Base and step are both proved, without using the lemma itself.
• S05.2 · premise_audit · subset_def, case_analysis — Comparability makes the two cases exhaustive; only transitivity of ⊆ and the induction hypothesis are used.
• S05.1 · premise_audit · subset_def — Only reflexivity of ⊆ is used.
• S05 · premise_audit · S04, L_chain_extremes — The lemma needs finiteness, nonemptiness and comparability, all confirmed.
• S04 · premise_audit · G1, subset_def — Only these four sets are claimed to form a chain; a general family need not (in τ₂, {a} and {b} are incomparable).
• S03 · premise_audit · G2, family_ops — Taking X for the intersection is a convention relative to the fixed underlying set (MKO assumption a2); without it ⋂∅ would be meaningless.
• S02 · premise_audit · G1, subset_def — The four members are checked one by one; no other condition is claimed.
• S01 · premise_audit · G1, G2, mko_topology_def — This step only unfolds the definition; failure of any one condition means 'not a topology'.

Error controls and negative controls

Not every family of subsets is a topology

The misconception the MKO names: treating any family of subsets as a topology. τ₂ contains ∅ and X and is closed under intersections, yet it is not a topology because {a}∪{b}={a,b}∉τ₂ (S10, S11). Every kind of condition must be checked.

Pairwise closure is not arbitrary closure

The other misconception the MKO names: taking closure under pairwise unions for closure under arbitrary unions. τ_fin is closed under pairwise unions (S13), but the union of the infinitely many singletons {0}, {2}, {4} and so on is the set of even numbers, which is not in τ_fin (S14). For a finite family containing ∅, every subfamily is finite and binary-union closure together with the empty-union condition suffices; without ∅ the empty subfamily can still fail; for τ₁ this guide uses the chain lemma to handle all subfamilies at once.

Do not forget the empty family

The axioms ∅∈τ and X∈τ are exactly the cases of the empty union and the empty intersection (S03). {{a},{a,b},X}, which lacks ∅, and {∅,{a},{a,b}}, which lacks X, are not topologies.

Finer and coarser compare families of open sets

τ₁⊆P(X) means P(X) is finer and τ₁ coarser; this is inclusion of families of open sets and has nothing to do with the size of X (MKO paragraph 2).

• τ₂={∅,{a},{b},X} contains ∅ and X and is closed under intersections, so it is a topology → reject — {a}∪{b}={a,b}∉τ₂, so the union condition fails.
• τ_fin is closed under pairwise unions, hence under arbitrary unions, so it is a topology on ℕ → reject — The union of the singletons {2k} is the set of even numbers, which is neither finite nor equal to ℕ.
• {{a},{a,b},X} is a topology on X → reject — It lacks ∅, that is, the union of the empty family is not in it; this alone refutes it.
• {∅,{a},{a,b}} is a topology on X → reject — It lacks X, that is, the intersection of the empty family (read as X) is not in it.
• τ₁ is finer than P(X) → reject — τ₁⊊P(X), so P(X) is finer; for example {b}∈P(X) but {b}∉τ₁.

Result and limitations

τ₁={∅,{a},{a,b},X} is a topology on X={a,b,c}: it is a chain, the union and intersection of a nonempty subfamily are its largest and smallest members, the empty family gives ∅ and X, and all 16 subfamilies are covered. τ₂={∅,{a},{b},X} is not a topology, since {a}∪{b}={a,b}∉τ₂, although it contains ∅ and X and is closed under intersections. {∅,X}⊊τ₁⊊P(X). On ℕ, τ_fin is closed under pairwise unions and finite intersections, but the set of even numbers is a union of its singletons and is not in τ_fin, so τ_fin is not a topology.

• finite_sets (a union of two finite sets is finite, a subset of a finite set is finite, a finite nonempty set of naturals has a largest element) is used as prerequisite knowledge and not proved here.
• The general remark needs its empty-family qualification: a finite family of sets that contains ∅ and is closed under binary unions is closed under unions of arbitrary subfamilies. Membership of ∅ handles the empty subfamily. This guide does not separately prove or use that general result; the complete proof for τ₁ still uses the chain lemma and treats the empty family separately.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 4da430d185bcefe3f83821030d9b54994119c5304ce3b95397b135d2151f8de7
• original source SHA-256: 9fc206f52faa8c93d175434ba7de7802035b74beb7ba12cd2a3c31cc736a538d
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)