English
Deleting a non-bridge edge from a connected graph preserves connectedness.
Русский
Удаление не-ребра-моста из связного графа сохраняет связность.
LaTeX
$$$ (hG : G.Connected) \\Rightarrow \\forall {x y : V}, \\neg G.IsBridge s(x,y) \\Rightarrow (G.deleteEdges {s(x,y)}).Connected $$$
Lean4
/-- Deleting a non-bridge edge from a connected graph preserves connectedness. -/
theorem connected_delete_edge_of_not_isBridge (hG : G.Connected) {x y : V} (h : ¬G.IsBridge s(x, y)) :
(G.deleteEdges {s(x, y)}).Connected := by
classical
simp only [isBridge_iff, not_and, not_not] at h
obtain hxy | hxy := em' <| G.Adj x y
· rwa [deleteEdges, Disjoint.sdiff_eq_left (by simpa)]
refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩
obtain ⟨P, hP⟩ := hG.exists_isPath w x
obtain heP | heP := em' <| s(x, y) ∈ P.edges
· exact ⟨(P.toDeleteEdges {s(x, y)} (by aesop)).reverse⟩
have hyP := P.snd_mem_support_of_mem_edges heP
let P₁ := P.takeUntil y hyP
have hxP₁ := Walk.endpoint_notMem_support_takeUntil hP hyP hxy.ne
have heP₁ : s(x, y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
exact (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x, y)} (by aesop)⟩)
