# Connected components: finding every component of a finite simple graph by complete BFS [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-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-connected-component-01 · production-20261019-adopted-96 ## Goal and scope Let G=(V,E) with V={0,1,2,3,4,5,6} and E consisting of exactly the five edges {0,1}, {0,2}, {1,2}, {3,4}, {4,5}. First prove that 'joined by a path' is an equivalence relation on V; then compute each equivalence class by complete BFS, prove that the set BFS returns is exactly that class, and conclude Q(G)={{0,1,2},{3,4,5},{6}}, where the isolated vertex 6 forms a singleton component. Works only inside the MKO's scope: a finite undirected loop-free simple graph with explicit labels 0 to 6 and a complete edge set (assumption a1), with reachability checked by complete BFS (assumption a2). It proves that connectivity is an equivalence relation, that BFS is correct (invariant, termination and closure) and that components are maximal. It does not treat weak or strong connectivity of directed graphs, component contraction or algorithmic complexity, and does not change the canonical MKO or its English edition. ## Givens and symbols - graph_basics - set_extensionality - subset_def - well_ordering - nat_induction - G1 — V={0,1,2,3,4,5,6}; E consists of exactly the five undirected edges {0,1}, {0,2}, {1,2}, {3,4}, {4,5}, with no loops and no multiple edges; this is the complete edge set (MKO assumption a1). - G2 — Walk: a vertex sequence (x_i)_{i=0}^{k} with k≥0 and {x_{i−1},x_i}∈E for every 1≤i≤k; its length is k. Path: a walk whose vertices x_i are pairwise distinct. For k=0, (x_0) is a path of length 0. - G3 — u∼v means there is a path from u to v (x_0=u, x_k=v). The component of v is [v]={w∈V ∣ v∼w}, and Q(G) is the set of all the [v] (MKO statement). - V,E — the vertex set and the undirected edge set - N(x) — the neighbour set {y ∣ {x,y}∈E} of x - u\sim v — there is a path between u and v - [v] — the class {w∈V ∣ v∼w} of v - R — the set of vertices visited by BFS - Q(G) — the set of all connected components of G ## Rules and sources - graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|. - 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). - well_ordering · prerequisite — Well-ordering principle: every nonempty subset of ℕ has a least element. - 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_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - 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. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a. - 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 uv holds; u0 give uwvw. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - 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. - 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. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_component_def · cited — In a finite undirected loop-free simple graph, u and v are connected if a path joins them; length-zero paths ensure reflexivity. The equivalence classes are the maximal connected components, mutually disjoint and covering every vertex. Isolated vertices form singleton components. · mko-connected-component - equiv_rel_def · prerequisite — Equivalence relation: a relation on a set that is reflexive (v∼v), symmetric (u∼v⇒v∼u) and transitive (u∼v and v∼w ⇒ u∼w). - bfs_procedure · prerequisite — BFS (start s): set R={s} and the queue to (s). While the queue is nonempty, remove its front vertex x and check every y in N(x) in increasing order: if y∉R, add y to R and append y to the queue. When the queue is empty, stop and return R. - L_walk_path · lemma — If there is a walk from u to w, there is a path from u to w. - L_classes_partition · lemma — For an equivalence relation ∼ on V: every v satisfies v∈[v], and if [u]∩[v]≠∅ then [u]=[v]. Hence the classes cover V and any two classes are equal or disjoint. - L_bfs_exact · lemma — In a finite loop-free simple graph, complete BFS from s stops, and the set R it returns equals [s]. ## Main derivation S01 · equivalentBefore E=\{\{0,1\},\{0,2\},\{1,2\},\{3,4\},\{4,5\}\} After N(0)=\{1,2\},\ N(1)=\{0,2\},\ N(2)=\{0,1\},\ N(3)=\{4\},\ N(4)=\{3,5\},\ N(5)=\{4\},\ N(6)=\varnothing Conditions: none Rule: graph_basics · Uses: G1 Leaf basis: graph_basics + set_builder + numeric_evaluation Read off each vertex's neighbours from the complete edge set: an undirected edge {a,b} puts b into N(a) and a into N(b). Vertex 6 occurs in no edge, so N(6)=∅. The degrees are 2, 2, 2, 1, 2, 1, 0 in order, summing to 10=2·5, in agreement with the handshake lemma (N1). S02 · impliesBefore v\in V After v\sim v Conditions: none Rule: def_unfold · Uses: G2, G3 Leaf basis: def_unfold + exists_intro For any vertex v, the one-term sequence (v) is a walk with k=0 (there is no edge to check), and its single vertex is trivially distinct from the others, so it is a path from v to v. Hence v∼v: reflexivity comes from the length-zero path and needs no loop (a simple graph has none anyway). S03 · impliesBefore u\sim v After v\sim u Conditions: none Rule: def_unfold · Uses: G2, G3 Leaf basis: def_unfold + graph_basics Take a path (x_i)_{i=0}^{k} from u to v and set y_i=x_{k−i}. Then y_0=v and y_k=u; each consecutive pair {y_{i−1},y_i}={x_{k−i+1},x_{k−i}} is an edge of the original path, because an undirected edge satisfies {a,b}={b,a}; the vertices are only reordered and stay pairwise distinct. So (y_i) is a path from v to u. S04 · impliesBefore u\sim v,\ v\sim w After \text{there is a walk from }u\text{ to }w Conditions: none Rule: def_unfold · Uses: G2, G3 Leaf basis: def_unfold + exists_elim Take a path (x_i)_{i=0}^{k} from u to v and a path (z_j)_{j=0}^{l} from v to w. Since x_k=v=z_0, joining them at v gives the sequence (x_0, x_1, up to x_k=z_0, z_1, up to z_l) of length k+l. Each consecutive pair is an edge of one of the two paths, so this is a walk from u to w. It need not be a path: the two pieces may share a vertex. Example: 0,1,2 and 2,1 join to 0,1,2,1, where vertex 1 repeats. S05 · impliesBefore \text{walk from }u\text{ to }w After u\sim w Conditions: none Rule: L_walk_path · Uses: S04 Leaf basis: well_ordering + contradiction + def_unfold By Lemma L_walk_path (proved in S05.1 and S05.2), the walk of S04 can be replaced by a path from u to w, so u∼w. Together with S04 this proves that ∼ is transitive. S06 · impliesBefore \sim\ \text{reflexive, symmetric, transitive} After \bigcup_{v\in V}[v]=V,\ \ [u]=[v]\ \lor\ [u]\cap[v]=\varnothing Conditions: none Rule: L_classes_partition · Uses: S02, S03, S05 Leaf basis: equiv_rel_def + set_extensionality By S02, S03 and S05, ∼ is an equivalence relation on V. By Lemma L_classes_partition (proved in S06.1 and S06.2), its classes cover V and any two classes are equal or disjoint. This is what the MKO means by 'mutually disjoint and covering every vertex'. S07 · impliesBefore R=\{0\},\ \text{queue }(0) After R=\{0,1,2\},\ \text{queue empty} Conditions: none Rule: bfs_procedure · Uses: S01, bfs_procedure Leaf basis: bfs_procedure + set_operations_def Run BFS from s=0. Remove 0: N(0)={1,2}; neither 1 nor 2 is in R, so both are added, R={0,1,2}, queue (1,2). Remove 1: N(1)={0,2} is already inside R. Remove 2: N(2)={0,1} is already inside R. The queue is empty, so BFS stops. There were 3 removals, and each one checked every neighbour of the removed vertex. S08 · theorem_applicationBefore R=\{0,1,2\}\ \text{(complete BFS from 0)} After [0]=\{0,1,2\} Conditions: G\ \text{finite, loop-free, simple}; \text{BFS run until the queue is empty} Rule: L_bfs_exact · Uses: S07, G1 Leaf basis: set_extensionality + nat_induction + bfs_procedure By Lemma L_bfs_exact (proved in S08.1 to S08.3), the set returned by complete BFS from s=0 is exactly [0]. So [0]={0,1,2}. S09 · theorem_applicationBefore R=\{3\},\ \text{queue }(3) After [3]=\{3,4,5\} Conditions: none Rule: L_bfs_exact · Uses: S01, S08 Leaf basis: bfs_procedure + set_extensionality 3 is the smallest vertex not in [0]. Remove 3: N(3)={4}, add 4. Remove 4: N(4)={3,5}; 3 is in R, add 5. Remove 5: N(5)={4} is in R. The queue is empty and R={3,4,5}; by L_bfs_exact, [3]={3,4,5}. S10 · impliesBefore N(6)=\varnothing After [6]=\{6\} Conditions: none Rule: L_bfs_exact · Uses: S01, S02, G2, G3 Leaf basis: bfs_procedure + def_unfold 6 is the only vertex outside [0]∪[3]. BFS removes 6, N(6)=∅, nothing is added, R={6}, so [6]={6}. Direct check: the first edge of a path of length at least 1 would contain 6, but no edge of E contains 6; so the only path from 6 is the length-zero path (6). An isolated vertex forms a singleton component and must not be dropped just because it is absent from the edge set. S11 · impliesBefore [0]=\{0,1,2\},\ [3]=\{3,4,5\},\ [6]=\{6\} After Q(G)=\{\{0,1,2\},\{3,4,5\},\{6\}\} Conditions: none Rule: L_classes_partition · Uses: S06, S08, S09, S10 Leaf basis: set_operations_def + finite_counting_basics + set_extensionality The three sets are pairwise disjoint and their union is V, with 3+3+1=7=|V| elements (N2). Take any class [v]: v lies in one of the three, say C, so v∈[v]∩C, and L_classes_partition gives [v]=C. So Q(G) consists of exactly these three classes; for example [1]=[2]=[0] and [4]=[5]=[3]. S12 · impliesBefore C=[v] After C\ \text{connected};\ C\subseteq S,\ S\ \text{connected}\Rightarrow S=C Conditions: none Rule: mko_component_def · Uses: S03, S05, G3 Leaf basis: set_extensionality + subset_def + def_unfold For a,b∈C, the relations v∼a and v∼b give an a-to-b path by symmetry and transitivity. Its vertices must also lie in C: for each vertex z along that path, concatenate a v-to-a path with the a-to-z prefix, then apply L_walk_path to obtain v∼z and hence z∈C. Thus the induced graph G[C] is connected, not merely ambient-connected. If a connected subset S contains C, every s∈S has a v-to-s path within S, also a path of the original graph; hence s∈[v]=C and S=C. For arbitrary subsets the internal-path requirement matters: {3,5} is connected in the ambient graph through 4 but its induced graph is disconnected. The set {0,1} is internally connected but properly contained in {0,1,2}, so it is not a component. S13 · impliesBefore \text{S06, S11, S12} After Q(G)=\{\{0,1,2\},\{3,4,5\},\{6\}\},\ \text{maximal, disjoint, covering }V Conditions: none Rule: mko_component_def · Uses: S06, S11, S12 Leaf basis: and_intro_elim + def_unfold ∼ is an equivalence relation (S06), its classes are exactly {0,1,2}, {3,4,5} and {6} (S11), and each class is a maximal connected set (S12). So the connected components of G are these three sets, mutually disjoint and covering every vertex, with the isolated vertex 6 as a singleton component. ## Substeps and lemmas S05.1 · impliesBefore \text{some walk from }u\text{ to }w After \text{a walk }(y_i)_{i=0}^{m}\text{ from }u\text{ to }w\text{ of least length }m Conditions: none Rule: well_ordering · Uses: G2, well_ordering Leaf basis: well_ordering + exists_elim The lengths of all walks from u to w form a subset of ℕ, nonempty because at least one walk exists. By the well-ordering principle it has a least element m; take a walk (y_i)_{i=0}^{m} of length m. S05.2 · impliesBefore (y_i)_{i=0}^{m}\ \text{shortest} After y_i\neq y_j\ (i