# Open and closed sets: classifying all sixteen subsets of a four-point topology [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-open-closed-set/) 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-open-closed-set-01 · production-20261019-adopted-96 ## Goal and scope Let X={1,2,3,4} and τ={∅,{1},{1,2},{3,4},{1,3,4},X}. First verify that τ is a topology on X, then list all closed sets and sort the sixteen subsets of X into four classes: clopen, open only, closed only, and neither; finally prove that in every topological space ∅ and X are clopen, and that the union of two closed sets is closed. Works inside the MKO's scope: the underlying set X and topology τ are fixed (assumption a1), and every complement is taken relative to the same X (assumption a2). The general results proved are only '∅ and X are always clopen' and 'the union of two closed sets is closed'; the dual statement for intersections of arbitrarily many closed sets is mentioned but not proved separately. The canonical MKO and its English edition are not changed. ## Givens and symbols - set_operations_def - set_extensionality - subset_def - finite_counting_basics - nat_induction - G1 — The underlying set X={1,2,3,4} (MKO assumption a1). - G2 — The family τ={∅,{1},{1,2},{3,4},{1,3,4},X}; every member is a subset of X. - G3 — Every complement is the complement X∖C relative to X, and every candidate set is first confirmed to be a subset of X (MKO assumption a2). - X — the underlying set {1,2,3,4} - \tau — the topology on X (the family of open sets) - \mathcal{C} — the family of closed sets {C⊆X ∣ X∖C∈τ} - X\setminus C — the complement of C relative to X - \mathcal{P}(X) — all subsets of X ## Rules and sources - 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. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈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. - 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₀. - topology_def · prerequisite — Topology: a family τ of open subsets of X containing ∅ and X, closed under arbitrary unions and finite intersections. - 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. - de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q. - 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. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - 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. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - mko_open_closed_def · cited — In a topological space (X,τ), a subset U⊆X is open exactly when U∈τ, and C⊆X is closed exactly when X∖C∈τ. Open and closed are not mutually exclusive; ∅ and X are always both open and closed. · mko-open-closed-set - mko_topological_space_def · cited — A topology on X is a family τ⊆P(X) with ∅∈τ, X∈τ, the union of any subfamily of τ in τ, and the intersection of any finite subfamily of τ in τ; the union of the empty family is ∅ and its intersection is read as X. · mko-topological-space - L_finite_family · lemma — Let τ be a finite family of subsets of X. If ∅∈τ and τ is closed under the union of two members, then the union of every subfamily of τ is in τ; if X∈τ and τ is closed under the intersection of two members, then the intersection of every subfamily of τ (the empty one read as X) is in τ. - L_double_complement · lemma — For every C⊆X, X∖(X∖C)=C. - L_demorgan · lemma — For A,B⊆X, X∖(A∪B)=(X∖A)∩(X∖B). ## Main derivation S01 · theorem_applicationBefore \tau=\{\varnothing,\{1\},\{1,2\},\{3,4\},\{1,3,4\},X\} After (X,\tau)\ \text{is a topological space} Conditions: \tau\ \text{finite}; \varnothing,X\in\tau Rule: L_finite_family · Uses: G1, G2 Leaf basis: topology_def + set_operations_def + nat_induction All six members of τ are subsets of X, and ∅∈τ, X∈τ. τ is a finite family, so by Lemma L_finite_family (proved in S01.1 and S01.2) it suffices to check that the union and intersection of any two members lie in τ to get closure under unions of every subfamily and intersections of every finite subfamily; this pairwise check is done in S01.3. So (X,τ) is a topological space, and only then can open and closed be discussed. S02 · equivalentBefore C\subseteq X\ \text{closed}\iff X\setminus C\in\tau After C\ \text{closed}\iff C=X\setminus U\ \text{for some}\ U\in\tau Conditions: C\subseteq X Rule: L_double_complement · Uses: S01, G3 Leaf basis: def_unfold + set_operations_def + set_extensionality By the MKO definition, C is closed exactly when X∖C∈τ. (⇒) Let U=X∖C∈τ; by L_double_complement, C=X∖(X∖C)=X∖U. (⇐) If C=X∖U with U∈τ, then X∖C=X∖(X∖U)=U∈τ. So the closed sets are exactly the complements of open sets, and the closed family can be computed by taking complements one by one. S03 · impliesBefore \{X\setminus U\mid U\in\tau\} After \mathcal{C}=\{X,\{2,3,4\},\{3,4\},\{1,2\},\{2\},\varnothing\} Conditions: none Rule: set_operations_def · Uses: S02, G2 Leaf basis: set_operations_def + injective_surjective_def Take complements one by one: X∖∅=X, X∖{1}={2,3,4}, X∖{1,2}={3,4}, X∖{3,4}={1,2}, X∖{1,3,4}={2}, X∖X=∅. By S02 these six sets are all the closed sets. Since taking complements undoes itself (L_double_complement), distinct open sets give distinct closed sets, so there are exactly 6 closed sets. S04 · impliesBefore \tau,\ \mathcal{C} After \tau\cap\mathcal{C}=\{\varnothing,\{1,2\},\{3,4\},X\} Conditions: none Rule: set_operations_def · Uses: G2, S03 Leaf basis: set_operations_def Comparing the two lists, the sets in both τ and 𝒞 are ∅, {1,2}, {3,4} and X; these four are clopen. Besides the inevitable ∅ and X, {1,2} and {3,4} are clopen too: they are complements of each other and both are open. S05 · impliesBefore \tau,\ \mathcal{C} After \tau\setminus\mathcal{C}=\{\{1\},\{1,3,4\}\} Conditions: none Rule: set_operations_def · Uses: G2, S03 Leaf basis: set_operations_def + mko_open_closed_def The members of τ not in 𝒞 are {1} and {1,3,4}: they are open, but their complements {2,3,4} and {2} are not in τ, so they are not closed. S06 · impliesBefore \tau,\ \mathcal{C} After \mathcal{C}\setminus\tau=\{\{2\},\{2,3,4\}\} Conditions: none Rule: set_operations_def · Uses: G2, S03 Leaf basis: set_operations_def + mko_open_closed_def The members of 𝒞 not in τ are {2} and {2,3,4}: they are closed but not open. S07 · impliesBefore |\mathcal{P}(X)|=2^4=16,\ |\tau\cup\mathcal{C}|=6+6-4=8 After \mathcal{P}(X)\setminus(\tau\cup\mathcal{C})=\{\{3\},\{4\},\{1,3\},\{1,4\},\{2,3\},\{2,4\},\{1,2,3\},\{1,2,4\}\} Conditions: none Rule: finite_counting_basics · Uses: S04, S05, S06 Leaf basis: finite_counting_basics + numeric_evaluation + set_operations_def X has 2^4=16 subsets. τ∪𝒞 has 6+6−4=8 members (the overlap is the 4 clopen sets of S04), so exactly 16−8=8 subsets are neither open nor closed, listed above. Check: 4 clopen, 2 open only, 2 closed only, 8 neither, total 16. Sub-step S07.1 checks {3} item by item. S08 · impliesBefore (Y,\sigma)\ \text{any topological space} After \varnothing\ \text{and}\ Y\ \text{are clopen in}\ (Y,\sigma) Conditions: none Rule: forall_intro · Uses: mko_topological_space_def, mko_open_closed_def Leaf basis: forall_intro + set_operations_def + mko_topological_space_def Take any topological space (Y,σ). By the definition of a topology, ∅∈σ and Y∈σ, so both are open. Also Y∖∅=Y∈σ, so ∅ is closed; Y∖Y=∅∈σ, so Y is closed. The proof uses no special property of Y or σ, so by generalization it holds for every topological space; in our example these are ∅ and X in S04. S09 · theorem_applicationBefore C_1,C_2\in\mathcal{C} After X\setminus(C_1\cup C_2)=(X\setminus C_1)\cap(X\setminus C_2)\in\tau,\ \text{so}\ C_1\cup C_2\in\mathcal{C} Conditions: C_1,C_2\subseteq X Rule: L_demorgan · Uses: S01, S02 Leaf basis: set_operations_def + de_morgan_logic + topology_def Let C1 and C2 be closed, so X∖C1 and X∖C2 are in τ. By the De Morgan lemma L_demorgan (proved in S09.1 and S09.2), X∖(C1∪C2)=(X∖C1)∩(X∖C2), an intersection of two open sets, which is in τ by the definition of a topology. So C1∪C2 is closed. The argument works in any topological space, and induction on the number of sets extends it to finitely many closed sets. S10 · impliesBefore \{2\},\ \{3,4\}\in\mathcal{C} After \{2\}\cup\{3,4\}=\{2,3,4\}\in\mathcal{C},\quad X\setminus\{2,3,4\}=\{1\}=\{1,3,4\}\cap\{1,2\} Conditions: none Rule: forall_elim · Uses: S09, S03 Leaf basis: forall_elim + set_operations_def Apply S09 to C1={2} and C2={3,4}: the union {2,3,4} should be closed. Direct check: X∖{2,3,4}={1}∈τ; by De Morgan it also equals (X∖{2})∩(X∖{3,4})={1,3,4}∩{1,2}={1}. The two computations agree. S11 · impliesBefore \text{claim:}\ C\ \text{closed}\iff C\notin\tau After \{1,2\}\in\tau\cap\mathcal{C},\ \{3\}\notin\tau\cup\mathcal{C}\ \Rightarrow\ \text{claim false in both directions} Conditions: none Rule: quantifier_negation · Uses: S04, S07.1 Leaf basis: quantifier_negation + iff_intro Test the misconception identified in the MKO 'closed means not open'. Counterexample to (⇒): {1,2} is closed and also open. Counterexample to (⇐): {3} is not open, and it is not closed either (S07.1). Both directions have counterexamples, so open and closed are independent properties and all four classes can occur. ## Substeps and lemmas S01.1 · induction_stepBefore F\subseteq\tau,\ |F|=k After \textstyle\bigcup F\in\tau\ \text{for every}\ k Conditions: \varnothing\in\tau; U,V\in\tau\Rightarrow U\cup V\in\tau Rule: nat_induction · Uses: nat_induction, set_operations_def, finite_counting_basics Leaf basis: nat_induction + set_operations_def + finite_counting_basics τ is finite, so every subfamily F is finite; induct on its number of members k. k=0: the union of the empty family is ∅, and ∅∈τ. k→k+1: pick a member U of F and let F′=F∖{U}, so |F′|=k and ∪F=(∪F′)∪U; by the induction hypothesis ∪F′∈τ, and closure under pairwise unions gives ∪F∈τ. This proves the union part of the lemma. S01.2 · induction_stepBefore F\subseteq\tau,\ |F|=k After \textstyle\bigcap F\in\tau\ \text{for every}\ k\ (\bigcap\varnothing=X) Conditions: X\in\tau; U,V\in\tau\Rightarrow U\cap V\in\tau Rule: nat_induction · Uses: nat_induction, set_operations_def, finite_counting_basics Leaf basis: nat_induction + set_operations_def Induct on k in the same way. k=0: the intersection of the empty family is read as X, and X∈τ. k→k+1: ∩F=(∩F′)∩U, and the induction hypothesis with closure under pairwise intersections gives ∩F∈τ. S01.1 and S01.2 together prove L_finite_family. S01.3 · impliesBefore U,V\in\tau After U\cup V\in\tau,\ U\cap V\in\tau Conditions: none Rule: set_operations_def · Uses: G2 Leaf basis: set_operations_def + finite_counting_basics Any pair involving ∅ or X returns to τ directly (∅∪A=A, ∅∩A=∅, X∪A=X, X∩A=A). The remaining six pairs: {1}∪{1,2}={1,2} with intersection {1}; {1}∪{3,4}={1,3,4} with intersection ∅; {1}∪{1,3,4}={1,3,4} with intersection {1}; {1,2}∪{3,4}=X with intersection ∅; {1,2}∪{1,3,4}=X with intersection {1}; {3,4}∪{1,3,4}={1,3,4} with intersection {3,4}. Every result is in τ. S02.1 · equivalentBefore x\in X\setminus(X\setminus C) After x\in C Conditions: C\subseteq X Rule: set_operations_def · Uses: set_operations_def, set_extensionality Leaf basis: set_operations_def + de_morgan_logic + set_extensionality x∈X∖(X∖C) ⇔ x∈X and not (x∈X and x∉C) ⇔ x∈X and x∈C ⇔ x∈C; the last step uses C⊆X. By extensionality, X∖(X∖C)=C, proving L_double_complement. S07.1 · impliesBefore \{3\} After \{3\}\notin\tau,\ X\setminus\{3\}=\{1,2,4\}\notin\tau Conditions: none Rule: mko_open_closed_def · Uses: G2, S03 Leaf basis: mko_open_closed_def + set_operations_def {3} is not among the six members of τ, so it is not open; its complement {1,2,4} is not in τ either, so {3} is not closed. {3} is neither open nor closed, which directly refutes 'not open means closed'. S09.1 · impliesBefore x\in X\setminus(A\cup B) After x\in(X\setminus A)\cap(X\setminus B) Conditions: none Rule: set_operations_def · Uses: set_operations_def, de_morgan_logic Leaf basis: set_operations_def + de_morgan_logic (⊆) x∈X∖(A∪B) means x∈X and not (x∈A or x∈B); by De Morgan in logic this is x∈X, x∉A and x∉B, so x∈X∖A and x∈X∖B. S09.2 · impliesBefore x\in(X\setminus A)\cap(X\setminus B) After x\in X\setminus(A\cup B);\ \text{hence}\ X\setminus(A\cup B)=(X\setminus A)\cap(X\setminus B) Conditions: none Rule: set_extensionality · Uses: S09.1, set_extensionality Leaf basis: set_operations_def + set_extensionality (⊇) If x∈X, x∉A and x∉B, then x is not in A∪B, so x∈X∖(A∪B). The two inclusions together give the equality by extensionality, proving L_demorgan. ## Reverse audits - S11 · premise_audit · S04, S07.1, quantifier_negation — Here each direction is refuted separately by a counterexample from the computations above; a counterexample to either one direction alone already suffices to refute the universal equivalence. - S10 · premise_audit · S09, S03, forall_elim — This is one instance of the general result and a cross-check; it cannot prove the general result in reverse. - S09.2 · premise_audit · S09.1, set_extensionality, set_operations_def — A set equality needs both inclusions, and both are proved. - S09.1 · premise_audit · set_operations_def, de_morgan_logic — This sub-step proves one inclusion only; the other is S09.2. - S09 · premise_audit · L_demorgan, mko_topological_space_def, mko_open_closed_def — It needs closure under finite intersections; nothing is claimed for unions of infinitely many closed sets (in general topologies they may fail to be closed). - S08 · premise_audit · mko_topological_space_def, mko_open_closed_def, forall_intro — Only two axioms of a topology and the definition of closed are used; it is not claimed that any other set must be clopen (for example {1} is not). - S07.1 · premise_audit · G2, mko_open_closed_def — Both verdicts use only the definition and the complete list of τ; the complement is computed in X. - S07 · premise_audit · S04, S05, S06, finite_counting_basics — The count uses inclusion and exclusion for the union (recomputable as N2, N3, N4). The eight listed sets appear in neither list, consistent with the count. - S06 · premise_audit · S03, G2 — 'Not open' comes from comparing with each of the six members of τ. - S05 · premise_audit · S03, set_operations_def — Each 'not closed' rests on the concrete check that the complement is not in τ. - S04 · premise_audit · G2, S03, set_operations_def — The intersection needs both complete lists; the conclusion is an equality of families. - S03 · premise_audit · S02, set_operations_def, L_double_complement — It needs the equivalence of S02 and the complete list of τ; every complement is computed inside X. - S02.1 · inverse_equivalence · set_operations_def, set_extensionality, de_morgan_logic — Each move is a logical equivalence (De Morgan, with x∈X known), so both directions hold. If C were not a subset of X, the last move would give only x∈C∩X and the formula would fail. - S02 · inverse_equivalence · L_double_complement, mko_open_closed_def — Both directions have reasons, using only the double complement and the definition. The complement must be relative to the same X, or the double complement formula fails. - S01.3 · premise_audit · G2, set_operations_def — The four nontrivial members form comb(4,2)=6 pairs, all listed (N1), with none omitted. - S01.2 · premise_audit · nat_induction, set_operations_def — It needs X∈τ as the base for the empty intersection, and closure under pairwise intersections. - S01.1 · premise_audit · nat_induction, set_operations_def, finite_counting_basics — The induction needs every subfamily to have finitely many members, which comes from τ being finite. The base case needs ∅∈τ; the empty family may not be skipped. - S01 · premise_audit · G2, L_finite_family, mko_topological_space_def — It needs τ finite, containing ∅ and X, and the pairwise check of S01.3. The lemma holds only for finite families; for an infinite family, closure under pairwise unions is not enough (see error control three). ## Error controls and negative controls Closed does not mean 'not open'The misconception identified in the MKO is reading 'closed' as 'not open'. Here {1,2} is both open and closed, and {3} is neither (S11). Closedness can only be decided by the definition: is the complement in τ? Complements must be taken in the same XIf the complement of {1,2} is wrongly taken in {1,2,3}, one gets {3}∉τ and wrongly concludes {1,2} is not closed; the correct X∖{1,2}={3,4}∈τ. If the complement of {3,4} is taken in {1,2,3,4,5}, one gets {1,2,5}, not even a subset of X, so comparing with τ is meaningless (MKO assumption a2). Pairwise closure suffices only for finite familiesS01 could check only pairwise unions because τ is finite (L_finite_family). Counterexample: the family of all finite subsets of ℕ together with ℕ itself contains ∅ and ℕ and is closed under pairwise unions and intersections, but the union of all {2k} is the set of even numbers, which is infinite and not equal to ℕ, so it is not in the family and the family is not a topology. - {3} is not open, so {3} is closed → reject — X∖{3}={1,2,4}∉τ, so {3} is not closed; it is neither open nor closed. - {1,2} is closed, so it is not open → reject — {1,2}∈τ, so it is both open and closed. - In {1,2,3,4,5} the complement of {3,4} is {1,2,5}∉τ, so {3,4} is not closed → reject — The complement must be taken in X: X∖{3,4}={1,2}∈τ, so {3,4} is closed. - The closed sets are exactly the 10 subsets not in τ → reject — There are only 6 closed sets (S03), and 4 of them are in τ; of the 10 subsets not in τ, 8 are not closed. ## Result and limitations τ is a topology on X={1,2,3,4}; the closed family is {X,{2,3,4},{3,4},{1,2},{2},∅}. The sixteen subsets split into: clopen ∅, {1,2}, {3,4}, X; open only {1}, {1,3,4}; closed only {2}, {2,3,4}; the other eight are neither open nor closed. In general, ∅ and X are clopen in every topological space, and the union of two closed sets is closed. - The dual statement in MKO paragraph 2, that an intersection of arbitrarily many closed sets is closed, follows from De Morgan's law for arbitrary families; this guide proves only the case of the union of two closed sets and does not write sub-steps for arbitrary families. ## Verification and source binding 4 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: db4ff6acc8064d0f256eceeebb39a241b3986504cee1fd23ae8da1de54588f78 - original source SHA-256: db4ff6acc8064d0f256eceeebb39a241b3986504cee1fd23ae8da1de54588f78 - 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-open-closed-set-01.json)