IsEdgeCut

theorem Graph.IsWalk.inter_setLinkEdges_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} {W : WList α β} (hWf : W.first ∈ S) (hWl : W.last ∉ S) (hW : G.IsWalk W) : (W.edgeSet ∩ E(G, S, G.vertexSet \ S)).Nonempty

theorem Graph.deleteEdges_setLinkEdge_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {S : Set α} (hx : x ∈ S) (hy : y ∉ S) : ¬(G.deleteEdges E(G, S, G.vertexSet \ S)).ConnBetween x y

theorem Graph.setLinkEdges_eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : S ⊆ G.vertexSet) : E(G, S, G.vertexSet \ S) = ∅ ↔ G[S].IsClosedSubgraph G

def Graph.IsEdgeCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Prop

A bond is a subset of edges that separates the graph into two connected components

Equations

• G.IsEdgeCut F = ∃ (S : Set α), E(G, S, G.vertexSet \ S) = F

theorem Graph.IsEdgeCut.exists {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsEdgeCut F) : ∃ S ⊆ G.vertexSet, E(G, S, G.vertexSet \ S) = F

theorem Graph.IsEdgeCut.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : G.IsEdgeCut F) : F ⊆ G.edgeSet

theorem Graph.isEdgeCut_map_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).IsEdgeCut F ↔ G.IsEdgeCut F

theorem Graph.isEdgeCut_edgeMap_image_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {β' : Type u_3} {σ : β → β'} (hσ : Set.InjOn σ G.edgeSet) (hF : F ⊆ G.edgeSet) : (G.edgeMap σ ⋯).IsEdgeCut (σ '' F) ↔ G.IsEdgeCut F

theorem Graph.isEdgeCut_edgeMap_image_iff_of_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {β' : Type u_3} {σ : β → β'} (hσ : Function.Injective σ) : (G.edgeMap σ ⋯).IsEdgeCut (σ '' F) ↔ G.IsEdgeCut F

theorem Graph.IsEdgeCut.exists_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {F : Set β} (he : G.IsLink e u v) (heF : e ∈ F) (hF : G.IsEdgeCut F) : ∃ S ⊆ G.vertexSet, E(G, S, G.vertexSet \ S) = F ∧ u ∈ S ∧ v ∉ S

theorem Graph.IsEdgeCut.not_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {e : β} {F : Set β} (hF : G.IsEdgeCut F) (he : e ∈ F) : ¬G.IsLoopAt e v

theorem Graph.IsEdgeCut.of_vert {α : Type u_1} {β : Type u_2} {G : Graph α β} (v : α) : G.IsEdgeCut E(G, {v}, G.vertexSet \ {v})

theorem Graph.IsEdgeCut.symmDiff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hF : G.IsEdgeCut F) (hF' : G.IsEdgeCut F') : G.IsEdgeCut (_root_.symmDiff F F')

theorem Graph.IsEdgeCut.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hHG : H ≤ G) (hF : G.IsEdgeCut F) : H.IsEdgeCut (H.edgeSet ∩ F)

theorem Graph.IsEdgeCut.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hGH : G.IsClosedSubgraph H) (hF : G.IsEdgeCut F) : H.IsEdgeCut F

theorem Graph.IsEdgeCut.not_connBetween_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {F : Set β} (he : G.IsLink e u v) (heF : e ∈ F) (hF : G.IsEdgeCut F) : ¬(G.deleteEdges F).ConnBetween u v

theorem Graph.IsEdgeCut.exists_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hFne : F.Nonempty) (hF : G.IsEdgeCut F) : ∃ (x : α) (y : α), G.ConnBetween x y ∧ ¬(G.deleteEdges F).ConnBetween x y

theorem Graph.isEdgeCut_subset_of_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {F : Set β} (hcon : G.ConnBetween x y) (hcon' : ¬(G.deleteEdges F).ConnBetween x y) : ∃ (F' : Set β), G.IsEdgeCut F' ∧ F' ⊆ F ∧ F'.Nonempty ∧ ¬(G.deleteEdges F').ConnBetween x y

theorem Graph.connBetween_deleteEdgesd_eq_iff_subset_not_isEdgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.ConnBetween = (G.deleteEdges F).ConnBetween ↔ ∀ F' ⊆ F, F'.Nonempty → ¬G.IsEdgeCut F'

Bridges

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

A bridge is a singleton edge separation

Equations

• G.IsBridge e = G.IsEdgeCut {e}

theorem Graph.IsBridge.isEdgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) : G.IsEdgeCut {e}

theorem Graph.IsBridge.mem_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) : e ∈ G.edgeSet

theorem Graph.IsLink.isBridge_iff_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (he : G.IsLink e x y) : G.IsBridge e ↔ ¬(G.deleteEdges {e}).ConnBetween x y

theorem Graph.IsLink.isBridge_iff_isEdgeCutBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (he : G.IsLink e x y) : G.IsBridge e ↔ G.IsEdgeCutBetween {e} x y

theorem Graph.IsBridge.anti_of_mem {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hHG : H ≤ G) (heH : e ∈ H.edgeSet) (he : G.IsBridge e) : H.IsBridge e

theorem Graph.not_isBridge_mono_of_mem {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hHG : H ≤ G) (he : ¬H.IsBridge e) (heH : e ∈ H.edgeSet) : ¬G.IsBridge e

theorem Graph.IsBridge.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hcle : H.IsClosedSubgraph G) (he : H.IsBridge e) : G.IsBridge e

theorem Graph.IsClosedSubgraph.isBridge_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (he : e ∈ H.edgeSet) (h : H.IsClosedSubgraph G) : G.IsBridge e ↔ H.IsBridge e

theorem Graph.IsBridge.singleton_linkEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (he : G.IsBridge e) (hl : G.IsLink e u v) : E(G, u, v) = {e}

theorem Graph.ConnBetween.deleteEdges_singleton_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (h : G.ConnBetween x y) (he : ¬G.IsBridge e) : (G.deleteEdges {e}).ConnBetween x y

theorem Graph.Preconnected.deleteEdges_singleton_preconnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.Preconnected) (he : ¬G.IsBridge e) : (G.deleteEdges {e}).Preconnected

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

theorem Graph.Preconnected.deleteEdges_singleton_preconnected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.Preconnected) : (G.deleteEdges {e}).Preconnected ↔ ¬G.IsBridge e

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

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

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

theorem Graph.Connected.isBridge_iff_isEdgeSep {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) (e : β) : G.IsBridge e ↔ G.IsEdgeSep {e}

theorem Graph.IsCompOf.deleteEdges_singleton_isCompOf {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (he : ¬G.IsBridge e) (h : H.IsCompOf G) : (H.deleteEdges {e}).IsCompOf (G.deleteEdges {e})

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

theorem Graph.IsPath.eq_of_isBridge_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {P : WList α β} (hP : G.IsPath P) (he : G.IsBridge e) (hl : G.IsLink e P.first P.last) : P = hl.walk

theorem Graph.IsLink.exists_cons_isCyclicWalk_of_not_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (hb : ¬G.IsBridge e) (hxy : G.IsLink e x y) : ∃ (C : WList α β), G.IsCyclicWalk (WList.cons x e C) ∧ C.first = y

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

theorem Graph.not_isBridge_of_exists_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hC : ∃ (C : WList α β), G.IsCyclicWalk C ∧ e ∈ C.edge) : ¬G.IsBridge e

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

@[simp]

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

theorem Graph.isBridge_iff_notMem_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ (C : WList α β), G.IsCyclicWalk C → e ∉ C.edge

def Graph.IsBond {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Prop

A bond of a graph is a minimal nonempty edge-cut.

Equations

• G.IsBond F = Minimal (fun (F : Set β) => G.IsEdgeCut F ∧ F.Nonempty) F

theorem Graph.IsBond.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : B ⊆ G.edgeSet

theorem Graph.IsBond.isEdgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : G.IsEdgeCut B

theorem Graph.IsBond.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : B.Nonempty

theorem Graph.IsBridge.isBond {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) : G.IsBond {e}

theorem Graph.isBridge_iff_isBond {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : G.IsBridge e ↔ G.IsBond {e}

theorem Graph.IsBond.isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {B : Set β} (heB : e ∈ B) (hB : G.IsBond B) : (G.deleteEdges (B \ {e})).IsBridge e

theorem Graph.IsBond.of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {B : Set β} (hGH : G.IsClosedSubgraph H) (hB : G.IsBond B) : H.IsBond B

theorem Graph.isBond_map_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).IsBond F ↔ G.IsBond F

theorem Graph.isBond_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {β' : Type u_3} {σ : β → β'} (hσ : Set.InjOn σ G.edgeSet) (hF : F ⊆ G.edgeSet) : (G.edgeMap σ ⋯).IsBond (σ '' F) ↔ G.IsBond F

theorem Graph.isBond_edgeMap_iff_of_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {β' : Type u_3} {σ : β → β'} (hσ : Function.Injective σ) : (G.edgeMap σ ⋯).IsBond (σ '' F) ↔ G.IsBond F

theorem Graph.isBond_edgeMap_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_3} {F : Set β'} {σ : β → β'} (hσ : Function.Injective σ) (hF : F ⊆ Set.range σ) : (G.edgeMap σ ⋯).IsBond F ↔ G.IsBond (σ ⁻¹' F)

theorem Graph.IsBond.exists_minimal_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {B : Set β} (hB : G.IsBond B) : ∃ (x : α) (y : α), G.ConnBetween x y ∧ Minimal (fun (F : Set β) => ¬(G.deleteEdges F).ConnBetween x y) B

theorem Graph.isBond_of_conn {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : S ⊆ G.vertexSet) (hScon : G[S].Preconnected) (hS'con : (G.deleteVerts S).Preconnected) (h : E(G, S, G.vertexSet \ S).Nonempty) : G.IsBond E(G, S, G.vertexSet \ S)

theorem Graph.PreconnGE.isBond_setLinkEdges_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} (hG : G.PreconnGE 2) (hv : v ∈ G.vertexSet) (hnt : G.vertexSet.Nontrivial) : G.IsBond E(G, {v}, G.vertexSet \ {v})

theorem Graph.walkable_deleteEdges_connBetween_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {B : Set β} : ((G.walkable x).deleteEdges B).ConnBetween x y ↔ (G.deleteEdges B).ConnBetween x y

theorem Graph.exists_isBond_subset_of_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {F : Set β} (hcon : G.ConnBetween x y) (hcon' : ¬(G.deleteEdges F).ConnBetween x y) : ∃ B ⊆ F, G.IsBond B ∧ ¬(G.deleteEdges B).ConnBetween x y

theorem Graph.IsEdgeCut.exists_isBond_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hne : F.Nonempty) (hF : G.IsEdgeCut F) : ∃ B ⊆ F, G.IsBond B

theorem Graph.IsEdgeCut.disjoint_union_isBond {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hfin : F.Finite) (hF : G.IsEdgeCut F) : ∃ (S : Set (Set β)), S.PairwiseDisjoint id ∧ ⋃₀ S = F ∧ ∀ B ∈ S, G.IsBond B

theorem Graph.edgeConnGE_iff_isEdgeCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hn : 1 ≤ n) : G.EdgeConnGE n ↔ G.Preconnected ∧ ∀ (F : Set β), G.IsEdgeCut F → F.Nonempty → ↑n ≤ F.encard

theorem Graph.edgeConnGE_iff_isBond {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hn : 1 ≤ n) : G.EdgeConnGE n ↔ G.Preconnected ∧ ∀ (b : Set β), G.IsBond b → ↑n ≤ b.encard

theorem Graph.EdgeConnGE.minDegreeGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hN : G.vertexSet.Nontrivial) (hn : G.EdgeConnGE n) : G.MinDegreeGE n