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.deleteVerts {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.deleteVerts {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.deleteVerts {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.deleteVerts {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.)

theorem Graph.Preconnected.left_mem_of_deleteEdges_linkEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Preconnected) (h' : ¬(G.deleteEdges E(G, u, v)).Preconnected) : u ∈ G.vertexSet

theorem Graph.Preconnected.right_mem_of_deleteEdges_linkEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Preconnected) (h' : ¬(G.deleteEdges E(G, u, v)).Preconnected) : v ∈ G.vertexSet

theorem Graph.IsClosedSubgraph.le_or_le_of_preconnected {α : Type u_1} {β : Type u_2} {G₁ G₂ H : Graph α β} (hH : H.Preconnected) (hHG : H ≤ G₂) (h12 : G₁.IsClosedSubgraph G₂) : H ≤ G₁ ∨ H ≤ G₂.deleteVerts G₁.vertexSet