ConnectivityStarter

Connected components through the public graph theory API

Open in Workbench View on GitHub

1-- Connected components through the public graph theory API.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module User.ConnectivityStarter8import Grace.Cumulus.GraphTheory910-- Components form a set-sized partition, even for infinite V.11theorem every_vertex_is_covered (V E : Set)12  shows ⋃(components(V, E)) = V13proof14  exact components.cover1516theorem overlap_forces_equality (V E x y z : Set)17  requires graph : SimpleGraph(V, E)18  requires hx : x ∈ V19  requires hy : y ∈ V20  requires first : z ∈ component(V, E, x)21  requires second : z ∈ component(V, E, y)22  shows component(V, E, x) = component(V, E, y)23proof24  exact component.equal_of_common_vertex with graph, hx, hy, first, second2526-- The connecting routes stay in the component itself.27theorem routes_stay_inside (V E x : Set)28  requires graph : SimpleGraph(V, E)29  requires hx : x ∈ V30  shows GraphConnected(component(V, E, x), inducedEdges(E, component(V, E, x)))31proof32  exact component.induced_connected with graph, hx3334theorem no_edges_between_components (V E x u v : Set)35  requires inside : u ∈ component(V, E, x)36  requires hv : v ∈ V37  requires outside : ¬(v ∈ component(V, E, x))38  shows ¬Adjacent(E, u, v)39proof40  exact component.no_crossing_edge with inside, hv, outside4142-- Opposite extremes: no edges give singleton components; all edges give V.43theorem isolated_components (V x : Set)44  requires hx : x ∈ V45  shows component(V, empty, x) = {x}46proof47  exact component.empty_graph with hx4849theorem complete_component (V x : Set)50  requires hx : x ∈ V51  shows component(V, completeEdges(V), x) = V52proof53  have connected := completeEdges.connected at V54  exact GraphConnected.component with connected, hx5556-- Every inhabited proper vertex subset of a connected graph has an exit edge.57theorem a_connected_graph_crosses_every_cut (V E A : Set)58  requires connected : GraphConnected(V, E)59  requires included : A ⊆ V60  requires inhabited : Nonempty(A)61  requires proper : A ≠ V62  shows ∃ u ∈ A, ∃ v ∈ V, ¬(v ∈ A) ∧ Adjacent(E, u, v)63proof64  exact GraphConnected.crossing_edge at V, E, A with *65