Main definitions #
SimpleGraph.Reachable
for the relation of whether there exists a walk between a given pair of verticesSimpleGraph.Preconnected
andSimpleGraph.Connected
are predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty.SimpleGraph.ConnectedComponent
is the type of connected components of a given graph.SimpleGraph.IsBridge
for whether an edge is a bridge edge
Main statements #
SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
characterizes bridge edges in terms of there being no cycle containing them.
Tags #
trails, paths, cycles, bridge edges
Two vertices are reachable if there is a walk between them.
This is equivalent to Relation.ReflTransGen
of G.Adj
.
See SimpleGraph.reachable_iff_reflTransGen
.
Instances For
The equivalence relation on vertices given by SimpleGraph.Reachable
.
Equations
- G.reachableSetoid = { r := G.Reachable, iseqv := ⋯ }
Instances For
A graph is preconnected if every pair of vertices is reachable from one another.
Equations
- G.Preconnected = ∀ (u v : V), G.Reachable u v
Instances For
A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.
There is a CoeFun
instance so that h u v
can be used instead of h.Preconnected u v
.
- preconnected : G.Preconnected
- nonempty : Nonempty V
Instances For
Equations
- G.instCoeFunConnectedForallForallReachable = { coe := ⋯ }
The quotient of V
by the SimpleGraph.Reachable
relation gives the connected
components of a graph.
Equations
Instances For
Gives the connected component containing a particular vertex.
Equations
- G.connectedComponentMk v = Quot.mk G.Reachable v
Instances For
Equations
- SimpleGraph.ConnectedComponent.inhabited = { default := G.connectedComponentMk default }
The ConnectedComponent
specialization of Quot.lift
. Provides the stronger
assumption that the vertices are connected by a path.
Equations
Instances For
This is Quot.recOn
specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices.
Equations
- SimpleGraph.ConnectedComponent.recOn c f h = Quot.recOn c f ⋯
Instances For
The map on connected components induced by a graph homomorphism.
Equations
- SimpleGraph.ConnectedComponent.map φ C = SimpleGraph.ConnectedComponent.lift (fun (v : V) => G'.connectedComponentMk (φ v)) ⋯ C
Instances For
An isomorphism of graphs induces a bijection of connected components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The set of vertices in a connected component of a graph.
Instances For
Equations
- SimpleGraph.ConnectedComponent.instSetLike = { coe := SimpleGraph.ConnectedComponent.supp, coe_injective' := ⋯ }
The equivalence between connected components, induced by an isomorphism of graphs, itself defines an equivalence on the supports of each connected component.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a connected component C
of a simple graph G
, produce the induced graph on C
.
The declaration connected_toSimpleGraph
shows it is connected, and toSimpleGraph_hom
provides the homomorphism back to G
.
Equations
- C.toSimpleGraph = SimpleGraph.induce C.supp G
Instances For
Homomorphism from a connected component graph to the original graph.
Equations
- C.toSimpleGraph_hom = { toFun := fun (u : ↥C) => ↑u, map_rel' := ⋯ }
Instances For
Alias of SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph
.
Get the walk between two vertices in a connected component from a walk in the original graph.
Equations
Instances For
There is a walk between every pair of vertices in a connected component.
Equations
- C.walk_toSimpleGraph hu hv = SimpleGraph.ConnectedComponent.walk_toSimpleGraph'✝ C hu hv (Nonempty.some ⋯)
Instances For
Alias of SimpleGraph.ConnectedComponent.connected_toSimpleGraph
.
Bridge edges #
An edge of a graph is a bridge if, after removing it, its incident vertices are no longer reachable from one another.
Equations
Instances For
Alias of SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem
.
Alias of SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem
.