Bridges

structure Graph.IsBridge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Prop

A bridge is an edge in no cycle

• mem_edgeSet : e ∈ G.edgeSet
• notMem_cycle ⦃C : WList α β⦄ : G.IsCycle C → e ∉ C.edge

theorem Graph.isBridge_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃C : WList α β⦄, G.IsCycle C → e ∉ C.edge

theorem Graph.not_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∈ G.edgeSet) : ¬G.IsBridge e ↔ ∃ (C : WList α β), G.IsCycle C ∧ e ∈ C.edge

theorem Graph.IsCycle.not_isBridge_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {C : WList α β} (hC : G.IsCycle C) (heC : e ∈ C.edge) : ¬G.IsBridge e

theorem Graph.IsLink.isBridge_iff_not_vertexConnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (he : G.IsLink e x y) : G.IsBridge e ↔ ¬(G.edgeDelete {e}).VertexConnected x y

theorem Graph.Connected.edgeDelete_singleton_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.Connected) (he : ¬G.IsBridge e) : (G.edgeDelete {e}).Connected

theorem Graph.Connected.edgeDelete_singleton_connected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.Connected) : (G.edgeDelete {e}).Connected ↔ ¬G.IsBridge e

theorem Graph.Connected.isBridge_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.Connected) : G.IsBridge e ↔ ¬(G.edgeDelete {e}).Connected

theorem Graph.IsPath.isBridge_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {P : WList α β} (hP : G.IsPath P) (heP : e ∈ P.edge) : P.toGraph.IsBridge e

Every edge of a path is a bridge

Staying Connected

theorem Graph.IsLeaf.eq_first_or_eq_last_of_mem_trail {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {P : WList α β} (hx : G.IsLeaf x) (hP : G.IsTrail P) (hxP : x ∈ P) : x = P.first ∨ x = P.last

A leaf vertex in a trail is either the first or last vertex of the trail

theorem Graph.IsLeaf.eq_first_or_eq_last_of_mem_path {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {P : WList α β} (hx : G.IsLeaf x) (hP : G.IsPath P) (hxP : x ∈ P) : x = P.first ∨ x = P.last

theorem Graph.IsLeaf.delete_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : G.IsLeaf x) (hG : G.Connected) : (G - {x}).Connected

theorem Graph.Connected.delete_first_connected_of_maximal_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.Connected) (hnt : G.vertexSet.Nontrivial) (hP : Maximal (fun (P : WList α β) => G.IsPath P) P) : (G - {P.first}).Connected

Deleting the first vertex of a maximal path of a connected graph gives a connected graph.

theorem Graph.Connected.delete_last_connected_of_maximal_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.Connected) (hnt : G.vertexSet.Nontrivial) (hP : Maximal (fun (P : WList α β) => G.IsPath P) P) : (G - {P.last}).Connected

Deleting the last vertex of a maximal path of a connected graph gives a connected graph.

theorem Graph.Connected.exists_delete_vertex_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.Connected) (hnt : G.vertexSet.Nontrivial) : ∃ x ∈ G.vertexSet, (G - {x}).Connected

Every finite connected graph on at least two vertices has a vertex whose deletion preserves its connectedness. (This requires a finite graph, since otherwise an infinite path is a counterexample.)