# Finding inclusion-maximal components from the complete subset table [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-topological-connected-component/) 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-connected-component-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Find every component of X={a,b,c}, tau={empty,{a},{b,c},X}. Use each induced topology, not a graph; do not extrapolate finite clopen components. ## Givens and symbols - sets - topology - definition_here - G1 — X={a,b,c}, tau={empty,{a},{b,c},X}; the empty space is connected by convention. - C_x — component containing x - \mathcal C — all connected subsets ## Rules and sources - mko_definition · cited — Finite families enumerate every induced subspace and connected subset. The union of all connected subsets containing x is its unique inclusion-maximal component. Then check that the components are pairwise equal or disjoint, cover X and are closed in the stated finite model. Finitely many closed components also make each component open, a finite-specific conclusion. In a general space components need not be open: in the rational subspace of the real line they are singletons and are not open. Do not substitute globally largest cardinality, graph components or a different structure on the same carrier. · mko-topological-connected-component - 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 — Subspace opens are ambient-open intersections; a connected subset has no nontrivial relative-open separation; the component of x is the union of all connected subsets containing x, equivalently the inclusion-maximal connected subset. ## Main derivation S01 · impliesBefore \{a\}\cap\{b,c\}=\varnothing,\quad\{a\}\cup\{b,c\}=X After \tau\text{ is a topology} Conditions: none Rule: topology · Uses: G1 Leaf basis: topology Apart from the complementary pair, operations with empty and whole stay in the family; every union/intersection axiom follows. S02 · definitionBefore \mathcal P(X) After \varnothing,\{a\},\{b\},\{c\},\{a,b\},\{a,c\},\{b,c\},X Conditions: none Rule: definition_here · Uses: G1 Leaf basis: definition_here List all eight subsets before computing their induced topologies. S03 · impliesBefore Y=\varnothing,\{a\},\{b\},\{c\} After \tau_\varnothing=\{\varnothing\},\quad\tau_{\{p\}}=\{\varnothing,\{p\}\} Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets The four small subsets have the listed induced topologies and no nontrivial separation. S04 · impliesBefore Y=\{a,b\},\{a,c\} After \tau_{\{a,b\}}=\mathcal P(\{a,b\}),\quad\tau_{\{a,c\}}=\mathcal P(\{a,c\}) Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets Ambient intersections give two-point discrete topologies, each separated by its two singletons and therefore disconnected. S05 · impliesBefore Y=\{b,c\},\ X After \tau_{\{b,c\}}=\{\varnothing,\{b,c\}\};\quad X=\{a\}\sqcup\{b,c\} Conditions: none Rule: sets · Uses: S01, S02 Leaf basis: sets The induced topology on {b,c} is indiscrete and connected; the two complementary nonempty opens explicitly separate X. S06 · definitionBefore \mathcal C=\{\varnothing,\{a\},\{b\},\{c\},\{b,c\}\} After C_a=\bigcup\{A\in\mathcal C:a\in A\}=\{a\};\quad C_b=C_c=\{b,c\} Conditions: none Rule: definition_here · Uses: S03, S04, S05 Leaf basis: definition_here Unite all connected subsets containing the given point, obtaining the unique inclusion-maximal candidates. S07 · impliesBefore \{C_a,C_b\}=\{\{a\},\{b,c\}\} After C_a\cap C_b=\varnothing,\quad C_a\cup C_b=X Conditions: none Rule: sets · Uses: S06 Leaf basis: sets The distinct components are disjoint and cover the entire carrier. S08 · impliesBefore X\setminus C_a=C_b\in\tau,\quad X\setminus C_b=C_a\in\tau After C_a,C_b\text{ both closed and open} Conditions: none Rule: sets · Uses: G1, S07 Leaf basis: sets Both components are closed and open in this finite model; this does not assert general components are open. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07 — In Q components are singletons but not open: an intermediate irrational separates any two rationals, while every rational neighborhood contains other rationals. - S07 · premise_audit · S06 — The duplicate C_c=C_b is normalized, not counted as a third component. - S06 · premise_audit · S03, S04, S05 — The smaller {a} is maximal: the larger {b,c} does not contain it. - S05 · premise_audit · S01, S02 — Connectedness has now been decided for all eight subsets. - S04 · premise_audit · S01, S02 — The complete four-set power sets are specified, rather than inferred from cardinality. - S03 · premise_audit · S01, S02 — The declared convention handles empty, and a singleton has only one nonempty set. - S02 · premise_audit · G1 — Maximality must use all candidates, not just large-looking sets. - S01 · premise_audit · G1 — The four-member list is complete. ## Error controls and negative controls Complete subset tableCheck all eight induced subspaces before inclusion-maximality. Maximal is not largestMaximal means no proper connected superset, not largest cardinality. - Only a largest-cardinality connected set is a component. → reject — {a} is smaller but remains inclusion-maximal. - {a,b} is connected. → reject — Its induced two-point discrete topology has a separation. - Components are open in every space. → reject — The singleton components of Q are not open, as justified at S08. ## Result and limitations The components {a} and {b,c} partition X and are clopen in this finite space. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 6e7ae0b999704533941449659c621f44afd0b89cb6a393c46fd149e31af15455 - original source SHA-256: f483b0fb384b4a7aa4bbe6cef26217d76cd52ab525b06d887513dadcd82709d5 - 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-topological-connected-component-01.json)