Vertex-Connectivity

structure Graph.VertexCut {α : Type u_1} {β : Type u_2} (G : Graph α β) : Type u_1

• carrier : Set α
• subset_vertexSet : self.carrier ⊆ G.vertexSet
• disconnects : ¬(G - self.carrier).Connected

instance Graph.instSetLikeVertexCut {α : Type u_1} {β : Type u_2} {G : Graph α β} : SetLike G.VertexCut α

Equations

• Graph.instSetLikeVertexCut = { coe := fun (x : G.VertexCut) => x.carrier, coe_injective' := ⋯ }

ST-Connectivity

structure Graph.STVertexCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : Type u_1

• carrier : Set α
• carrier_subset : self.carrier ⊆ G.vertexSet
• left_subset : S ⊆ G.vertexSet
• right_subset : T ⊆ G.vertexSet
• ST_disconnects (s : α) : s ∈ S → ∀ t ∈ T, ¬(G - self.carrier).VertexConnected s t

instance Graph.instSetLikeSTVertexCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : SetLike (G.STVertexCut S T) α

Equations

• Graph.instSetLikeSTVertexCut = { coe := fun (x : G.STVertexCut S T) => x.carrier, coe_injective' := ⋯ }

def Graph.sTVertexCut_of_left {α : Type u_1} {β : Type u_2} {S T : Set α} (G : Graph α β) (hS : S ⊆ G.vertexSet) (hT : T ⊆ G.vertexSet) : G.STVertexCut S T

Equations

• G.sTVertexCut_of_left hS hT = { carrier := S, carrier_subset := hS, left_subset := hS, right_subset := hT, ST_disconnects := ⋯ }

def Graph.sTVertexCut_of_right {α : Type u_1} {β : Type u_2} {S T : Set α} (G : Graph α β) (hS : S ⊆ G.vertexSet) (hT : T ⊆ G.vertexSet) : G.STVertexCut S T

Equations

• G.sTVertexCut_of_right hS hT = { carrier := T, carrier_subset := hT, left_subset := hS, right_subset := hT, ST_disconnects := ⋯ }

st-Connectivity

structure Graph.stCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (X : Set α) : Prop

• left_not_mem : s ∉ X
• right_not_mem : t ∉ X
• not_vertexConnected : ¬(G - X).VertexConnected s t

theorem Graph.stCut_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (X : Set α) : G.stCut s t X ↔ s ∉ X ∧ t ∉ X ∧ ¬(G - X).VertexConnected s t

@[simp]

theorem Graph.stCut_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} : G.stCut s t ∅ ↔ ¬G.VertexConnected s t

theorem Graph.Adj.not_stCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {X : Set α} (h : G.Adj s t) : ¬G.stCut s t X

theorem Graph.stCut.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s t : α} {X : Set α} (h : G.stCut s t X) (hle : H ≤ G) : H.stCut s t X

def Graph.stVxPreConn {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (n : Cardinal.{u_1}) : Prop

Equations

• G.stVxPreConn s t n = ∀ (X : Set α), G.stCut s t X → n ≤ Cardinal.mk ↑X

@[simp]

theorem Graph.stVxPreConn_zero {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) : G.stVxPreConn s t 0

theorem Graph.stVxPreConn.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s t : α} {n : Cardinal.{u_1}} (h : H.stVxPreConn s t n) (hle : H ≤ G) : G.stVxPreConn s t n

theorem Graph.stVxPreConn.anti_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n m : Cardinal.{u_1}} (hle : n ≤ m) (h : G.stVxPreConn s t m) : G.stVxPreConn s t n

theorem Graph.stVxPreConn_iff_forall_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : Cardinal.{u_1}} : G.stVxPreConn s t n ↔ ∀ (X : Set α), Cardinal.mk ↑X < n → ¬G.stCut s t X

@[simp]

theorem Graph.stVxPreConn_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} : G.stVxPreConn s t 1 ↔ G.VertexConnected s t

def Graph.internallyDisjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (s t : α) {ι : Type u_5} (f : ι → G.Subgraph) : Prop

Equations

• Graph.internallyDisjoint s t f = Pairwise fun (i j : ι) => (↑(f i)).vertexSet ∩ (↑(f j)).vertexSet = {s, t}

structure Graph.stEnsemble {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (ι : Type u_5) : Type (max (max u_1 u_2) u_5)

• f : ι → G.Subgraph
• internallyDisjoint : Graph.internallyDisjoint s t self.f
• stConnected (i : ι) : (↑(self.f i)).VertexConnected s t

def Graph.stEnsemble.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {ι : Type u_3} {s t : α} (P : H.stEnsemble s t ι) (hle : H ≤ G) : G.stEnsemble s t ι

Equations

• P.of_le hle = { f := fun (x : ι) => (P.f x).of_le hle, internallyDisjoint := ⋯, stConnected := ⋯ }

def Graph.stEmsemble.precomp {α : Type u_1} {β : Type u_2} {G : Graph α β} {ι : Type u_3} {ι' : Type u_4} {s t : α} (P : G.stEnsemble s t ι) (f : ι' ↪ ι) : G.stEnsemble s t ι'

Equations

• Graph.stEmsemble.precomp P f = { f := P.f ∘ ⇑f, internallyDisjoint := ⋯, stConnected := ⋯ }

def Graph.STVxConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (n : Cardinal.{u_1}) : Prop

Equations

• G.STVxConnectivity s t n = IsGreatest {m : Cardinal.{?u.28} | m ≤ Cardinal.mk ↑G.vertexSet ∧ G.stVxPreConn s t m} n