Connectivity between two sets

def Graph.SetConnected {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : Prop

Equations

• G.SetConnected S T = ∃ s ∈ S, ∃ t ∈ T, G.ConnBetween s t

@[simp]

theorem Graph.SetConnected_singleton {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) : G.SetConnected {s} {t} ↔ G.ConnBetween s t

theorem Graph.SetConnected.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S T : Set α} (h : G.SetConnected S T) (hle : G ≤ H) : H.SetConnected S T

theorem Graph.SetConnected.subset_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' T : Set α} (h : G.SetConnected S T) (hS : S ⊆ S') : G.SetConnected S' T

theorem Graph.SetConnected.subset_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T T' : Set α} (h : G.SetConnected S T) (hT : T ⊆ T') : G.SetConnected S T'

theorem Graph.SetConnected.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' T T' : Set α} (h : G.SetConnected S T) (hS : S ⊆ S') (hT : T ⊆ T') : G.SetConnected S' T'

theorem Graph.setConnected_refl {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (h : ¬Disjoint G.vertexSet S) : G.SetConnected S S

theorem Graph.SetConnected.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnected S T) : G.SetConnected T S

theorem Graph.setConnected_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.SetConnected S T ↔ G.SetConnected T S

theorem Graph.SetConnected.vertexSet_inter_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnected S T) : G.SetConnected (G.vertexSet ∩ S) T

theorem Graph.SetConnected.vertexSet_inter_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnected S T) : G.SetConnected S (G.vertexSet ∩ T)

theorem Graph.SetConnected.vertexSet_inter {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnected S T) : G.SetConnected (G.vertexSet ∩ S) (G.vertexSet ∩ T)

@[simp]

theorem Graph.setConnected_left_union_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' T : Set α} : G.SetConnected (S ∪ S') T ↔ G.SetConnected S T ∨ G.SetConnected S' T

@[simp]

theorem Graph.setConnected_right_union_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T T' : Set α} : G.SetConnected S (T ∪ T') ↔ G.SetConnected S T ∨ G.SetConnected S T'

theorem Graph.IsWalkFrom.SetConnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {W : WList α β} (hW : G.IsWalkFrom S T W) : G.SetConnected S T

theorem Graph.setConnected_iff_exists_isWalkFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) : G.SetConnected S T ↔ ∃ (W : WList α β), G.IsWalkFrom S T W

theorem Graph.SetConnected.exists_isWalkFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) : G.SetConnected S T → ∃ (W : WList α β), G.IsWalkFrom S T W

Alias of the forward direction of Graph.setConnected_iff_exists_isWalkFrom.

theorem Graph.setConnected_iff_exists_isPathFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) : G.SetConnected S T ↔ ∃ (P : WList α β), G.IsPathFrom S T P

theorem Graph.SetConnected.exists_isPathFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) : G.SetConnected S T → ∃ (P : WList α β), G.IsPathFrom S T P

Alias of the forward direction of Graph.setConnected_iff_exists_isPathFrom.

theorem Graph.ConnBetween.neighbor_setConnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : G.ConnBetween s t) (hne : s ≠ t) (hadj : ¬G.Adj s t) : (G.deleteVerts {s, t}).SetConnected (N(G, s) \ {s}) (N(G, t) \ {t})

Cut between two sets

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

• subset_vertexSet : C ⊆ G.vertexSet
• ST_disconnects : ¬(G.deleteVerts C).SetConnected S T

theorem Graph.isSetCut_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T C : Set α) : G.IsSetCut S T C ↔ C ⊆ G.vertexSet ∧ ¬(G.deleteVerts C).SetConnected S T

theorem Graph.isSetCut_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : ¬G.SetConnected S T) : G.IsSetCut S T ∅

theorem Graph.left_isSetCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.IsSetCut S T (G.vertexSet ∩ S)

theorem Graph.right_isSetCut {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.IsSetCut S T (G.vertexSet ∩ T)

theorem Graph.IsSetCut.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} (h : G.IsSetCut S T C) : G.IsSetCut T S C

theorem Graph.isSetCut_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} : G.IsSetCut S T C ↔ G.IsSetCut T S C

theorem Graph.IsSetCut.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C S T : Set α} (h : G.IsSetCut S T C) (hle : H ≤ G) : H.IsSetCut S T (H.vertexSet ∩ C)

theorem Graph.IsSetCut.anti_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S S' T : Set α} (h : G.IsSetCut S T C) (hS : S' ⊆ S) : G.IsSetCut S' T C

theorem Graph.IsSetCut.anti_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T T' : Set α} (h : G.IsSetCut S T C) (hT : T' ⊆ T) : G.IsSetCut S T' C

theorem Graph.IsSetCut.anti {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S S' T T' : Set α} (h : G.IsSetCut S T C) (hS : S' ⊆ S) (hT : T' ⊆ T) : G.IsSetCut S' T' C

theorem Graph.IsSetCut.left_union {α : Type u_1} {β : Type u_2} {G : Graph α β} {C C' S S' T : Set α} (h₁ : G.IsSetCut S T C) (h₂ : G.IsSetCut S' T C') : G.IsSetCut (S ∪ S') T (C ∪ C')

theorem Graph.IsSetCut.right_union {α : Type u_1} {β : Type u_2} {G : Graph α β} {C C' S T T' : Set α} (h₁ : G.IsSetCut S T C) (h₂ : G.IsSetCut S T' C') : G.IsSetCut S (T ∪ T') (C ∪ C')

theorem Graph.isSetCut_vertexSet_inter_left_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} : G.IsSetCut (G.vertexSet ∩ S) T C ↔ G.IsSetCut S T C

theorem Graph.IsSetCut.vertexSet_inter_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} : G.IsSetCut S T C → G.IsSetCut (G.vertexSet ∩ S) T C

Alias of the reverse direction of Graph.isSetCut_vertexSet_inter_left_iff.

theorem Graph.isSetCut_vertexSet_inter_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} : G.IsSetCut S (G.vertexSet ∩ T) C ↔ G.IsSetCut S T C

theorem Graph.IsSetCut.vertexSet_inter_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} : G.IsSetCut S T C → G.IsSetCut S (G.vertexSet ∩ T) C

Alias of the reverse direction of Graph.isSetCut_vertexSet_inter_right_iff.

theorem Graph.IsSetCut.of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T X : Set α} (h : (G.deleteVerts X).IsSetCut S T C) : G.IsSetCut S T (X ∩ G.vertexSet ∪ C)

theorem Graph.IsSetCut.of_deleteVerts' {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T X : Set α} (hC : (G.deleteVerts X).IsSetCut S T C) : G.IsSetCut (S ∪ X) (T ∪ X) (X ∩ G.vertexSet ∪ C)

theorem Graph.IsWalkFrom.not_disjoint_isSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {W : WList α β} (hW : G.IsWalkFrom S T W) (hC : G.IsSetCut S T C) : ¬Disjoint W.vertexSet C

theorem Graph.IsWalkFrom.exists_mem_isSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {W : WList α β} (hW : G.IsWalkFrom S T W) (hC : G.IsSetCut S T C) : ∃ v ∈ W, v ∈ C

theorem Graph.IsSetCut.not_disjoint_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {C S T : Set α} {W : WList α β} (hW : G.IsWalk W) (hu : u ∈ W.vertexSet ∩ S) (hv : v ∈ W.vertexSet ∩ T) (hC : G.IsSetCut S T C) : ¬Disjoint W.vertexSet C

theorem Graph.IsSetCut.exists_mem_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {C S T : Set α} {W : WList α β} (hW : G.IsWalk W) (hu : u ∈ W.vertexSet ∩ S) (hv : v ∈ W.vertexSet ∩ T) (hC : G.IsSetCut S T C) : ∃ v ∈ W, v ∈ C

theorem Graph.IsSetCut.left_trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {C U S T : Set α} (h₁ : G.IsSetCut S T C) (h₂ : G.IsSetCut C T U) : G.IsSetCut S T U

theorem Graph.IsSetCut.right_trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {C U S T : Set α} (h₁ : G.IsSetCut S T C) (h₂ : G.IsSetCut S C U) : G.IsSetCut S T U

theorem Graph.IsSetCut.inter_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} (hC : G.IsSetCut S T C) : G.vertexSet ∩ S ∩ T ⊆ C

theorem Graph.IsSetCut.subset_of_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {U S : Set α} (hC : G.IsSetCut S S U) : G.vertexSet ∩ S ⊆ U

@[simp]

theorem Graph.isSetCut_self_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {U S : Set α} (hU : U ⊆ G.vertexSet) : G.IsSetCut S S U ↔ G.vertexSet ∩ S ⊆ U

theorem Graph.IsSepBetween.isSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {C : Set α} (hC : G.IsSepBetween s t C) : G.IsSetCut (insert s C) (insert t C) C

theorem Graph.IsSetCut.left_diff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} (hC : G.IsSetCut S T C) : G.IsSetCut (S \ C) T C

theorem Graph.IsSetCut.right_diff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} (hC : G.IsSetCut S T C) : G.IsSetCut S (T \ C) C

theorem Graph.IsSetCut.prefixUntil_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {P : WList α β} [DecidablePred fun (x : α) => x ∈ C] (hP : G.IsWalk P) (hPf : P.first ∈ S) (hPl : P.last ∈ T) (hC : G.IsSetCut S T C) : Disjoint (P.prefixUntil fun (x : α) => x ∈ C).vertexSet (T \ C)

theorem Graph.IsSetCut.suffixFrom_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {P : WList α β} [DecidablePred fun (x : α) => x ∈ C] (hP : G.IsWalk P) (hPf : P.first ∈ S) (hPl : P.last ∈ T) (hC : G.IsSetCut S T C) : Disjoint (P.suffixFromLast fun (x : α) => x ∈ C).vertexSet (S \ C)

theorem Graph.IsSetCut.prefixUntil_isWalk_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {P : WList α β} [DecidablePred fun (x : α) => x ∈ C] (hP : G.IsWalk P) (hPf : P.first ∈ S) (hPl : P.last ∈ T) (hC : G.IsSetCut S T C) : (G.deleteVerts (T \ C)).IsWalk (P.prefixUntil fun (x : α) => x ∈ C)

theorem Graph.IsSetCut.suffixFrom_isWalk_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {C S T : Set α} {P : WList α β} [DecidablePred fun (x : α) => x ∈ C] (hP : G.IsWalk P) (hPf : P.first ∈ S) (hPl : P.last ∈ T) (hC : G.IsSetCut S T C) : (G.deleteVerts (S \ C)).IsWalk (P.suffixFromLast fun (x : α) => x ∈ C)

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

• subset_edgeSet : C ⊆ G.edgeSet
• ST_disconnects : ¬(G.deleteEdges C).SetConnected S T

theorem Graph.isEdgeSetCut_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : ¬G.SetConnected S T) : G.IsEdgeSetCut S T ∅

theorem Graph.IsWalkFrom.not_disjoint_isEdgeSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {F : Set β} {W : WList α β} (hW : G.IsWalkFrom S T W) (hC : G.IsEdgeSetCut S T F) : ¬Disjoint W.edgeSet F

theorem Graph.IsWalkFrom.exists_mem_isEdgeSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {F : Set β} {W : WList α β} (hW : G.IsWalkFrom S T W) (hC : G.IsEdgeSetCut S T F) : ∃ e ∈ W.edgeSet, e ∈ F

theorem Graph.IsEdgeSetCut.disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {F : Set β} (hF : G.IsEdgeSetCut S T F) : Disjoint G.vertexSet (S ∩ T)

theorem Graph.not_isEdgeSetCut_of_not_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {F : Set β} (hdj : ¬Disjoint G.vertexSet (S ∩ T)) : ¬G.IsEdgeSetCut S T F

noncomputable def Graph.inc_vert {α : Type u_1} {β : Type u_2} {G : Graph α β} (e : ↑G.edgeSet) : α

Equations

• Graph.inc_vert e = ⋯.choose

@[simp]

theorem Graph.inc_vert_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} (e : ↑G.edgeSet) : G.Inc (↑e) (inc_vert e)

theorem Graph.inc_vert_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} (e : ↑G.edgeSet) : inc_vert e ∈ G.vertexSet

theorem Graph.IsEdgeSetCut.isSetCut {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {F : Set β} (hF : G.IsEdgeSetCut S T F) : G.IsSetCut S T (inc_vert '' Subtype.val ⁻¹' F)

Ensemble of paths between two sets

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

• paths : Set (WList α β)
• disjoint : self.paths.Pairwise (Function.onFun Disjoint WList.vertexSet)
• valid ⦃P : WList α β⦄ : P ∈ self.paths → G.IsPath P

def Graph.SetEnsemble.between {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) (S T : Set α) : Prop

Equations

• A.between S T = ∀ ⦃P : WList α β⦄, P ∈ A.paths → G.IsPathFrom S T P

def Graph.SetEnsemble.vertexPartition {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : Partition (Set α)

Equations

• A.vertexPartition = Partition.ofPairwiseDisjoint' ⋯ ⋯

@[simp]

theorem Graph.SetEnsemble.vertexSet_mem_vertexPartition {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (A : G.SetEnsemble) (hP : P ∈ A.paths) : P.vertexSet ∈ A.vertexPartition

def Graph.SetEnsemble.vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : Set α

Equations

• A.vertexSet = A.vertexPartition.supp

@[simp]

theorem Graph.SetEnsemble.mem_vertexSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} (A : G.SetEnsemble) : v ∈ A.vertexSet ↔ ∃ P ∈ A.paths, v ∈ P

@[simp]

theorem Graph.SetEnsemble.subset_vertexSet_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} {A : G.SetEnsemble} (hP : P ∈ A.paths) : P.vertexSet ⊆ A.vertexSet

theorem Graph.SetEnsemble.vertexSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : A.vertexSet ⊆ G.vertexSet

theorem Graph.SetEnsemble.vertexSet_eq_biUnion {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : A.vertexSet = ⋃ P ∈ A.paths, P.vertexSet

theorem Graph.SetEnsemble.image_first_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : WList.first '' A.paths ⊆ A.vertexSet

theorem Graph.SetEnsemble.image_last_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) : WList.last '' A.paths ⊆ A.vertexSet

def Graph.SetEnsemble.empty {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.SetEnsemble

Equations

• Graph.SetEnsemble.empty G = { paths := ∅, disjoint := ⋯, valid := ⋯ }

@[simp]

theorem Graph.SetEnsemble.empty_paths {α : Type u_1} {β : Type u_2} (G : Graph α β) : (empty G).paths = ∅

@[simp]

theorem Graph.SetEnsemble.empty_between {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) : (empty G).between S T

def Graph.SetEnsemble.single {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : G.SetEnsemble

Equations

• Graph.SetEnsemble.single hP = { paths := {P}, disjoint := ⋯, valid := ⋯ }

@[simp]

theorem Graph.SetEnsemble.single_between {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {P : WList α β} (hP : G.IsPathFrom S T P) : (single ⋯).between S T

noncomputable def Graph.SetEnsemble.of_vertex {α : Type u_1} {β : Type u_2} {G : Graph α β} (A : G.SetEnsemble) (v : α) (hv : v ∈ A.vertexSet) : WList α β

Equations

• A.of_vertex v hv = Exists.choose ⋯

@[simp]

theorem Graph.SetEnsemble.of_vertex_mem_setEnsemble {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {A : G.SetEnsemble} (hv : v ∈ A.vertexSet) : A.of_vertex v hv ∈ A.paths

@[simp]

theorem Graph.SetEnsemble.mem_of_vertex {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {A : G.SetEnsemble} (hv : v ∈ A.vertexSet) : v ∈ A.of_vertex v hv

theorem Graph.SetEnsemble.eq_of_vertex_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {P : WList α β} {A : G.SetEnsemble} (hv : v ∈ A.vertexSet) (hP : P ∈ A.paths) (hvP : v ∈ P) : P = A.of_vertex v hv

theorem Graph.SetEnsemble.of_vertex_injOn_first {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {A : G.SetEnsemble} (hu : u ∈ WList.first '' A.paths) (hv : v ∈ WList.first '' A.paths) : A.of_vertex u ⋯ = A.of_vertex v ⋯ ↔ u = v

theorem Graph.SetEnsemble.of_vertex_injOn_last {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {A : G.SetEnsemble} (hu : u ∈ WList.last '' A.paths) (hv : v ∈ WList.last '' A.paths) : A.of_vertex u ⋯ = A.of_vertex v ⋯ ↔ u = v

theorem Graph.SetEnsemble.between.image_last_eq_inter {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {A : G.SetEnsemble} (hAST : A.between S T) : WList.last '' A.paths = T ∩ A.vertexSet

theorem Graph.SetEnsemble.between.image_first_eq_inter {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} {A : G.SetEnsemble} (hAST : A.between S T) : WList.first '' A.paths = S ∩ A.vertexSet

k-connectivity between two sets

noncomputable def Graph.setConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : ℕ∞

Minimum C.encard over vertex set cuts C between S and T, as an ℕ∞.

Equations

• G.setConnectivity S T = ⨅ (C : { C : Set α // G.IsSetCut S T C }), (↑C).encard

theorem Graph.le_setConnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} (S T : Set α) : k ≤ G.setConnectivity S T ↔ ∀ ⦃C : Set α⦄, G.IsSetCut S T C → k ≤ C.encard

theorem Graph.setConnectivity_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.setConnectivity S T = G.setConnectivity T S

@[simp]

theorem Graph.setConnectivity_vertexSet_inter_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.setConnectivity (G.vertexSet ∩ S) T = G.setConnectivity S T

@[simp]

theorem Graph.setConnectivity_vertexSet_inter_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.setConnectivity S (G.vertexSet ∩ T) = G.setConnectivity S T

@[simp]

theorem Graph.one_le_setConnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : 1 ≤ G.setConnectivity S T ↔ G.SetConnected S T

theorem Graph.setConnectivity_le_deleteVert_add_encard {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T X : Set α) : G.setConnectivity S T ≤ (G.deleteVerts X).setConnectivity (S \ X) (T \ X) + (X ∩ G.vertexSet).encard

theorem Graph.setConnectivity_left_mono {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' T : Set α} (hS : S ⊆ S') : G.setConnectivity S T ≤ G.setConnectivity S' T

theorem Graph.setConnectivity_right_mono {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T T' : Set α} (hT : T ⊆ T') : G.setConnectivity S T ≤ G.setConnectivity S T'

theorem Graph.setConnectivity_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) (S T : Set α) : G.setConnectivity S T ≤ H.setConnectivity S T

theorem Graph.inter_encard_le_setConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : (G.vertexSet ∩ S ∩ T).encard ≤ G.setConnectivity S T

theorem Graph.setConnectivity_le_inter_left_encard {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.setConnectivity S T ≤ (G.vertexSet ∩ S).encard

theorem Graph.setConnectivity_le_inter_right_encard {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.setConnectivity S T ≤ (G.vertexSet ∩ T).encard

theorem Graph.setConnectivity_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} : G.setConnectivity S S = (G.vertexSet ∩ S).encard

def Graph.SetConnGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (n : ℕ) : Prop

Equations

• G.SetConnGE S T n = ∀ ⦃C : Set α⦄, G.IsSetCut S T C → ↑n ≤ C.encard

theorem Graph.setConnGE_iff_le_setConnectivity {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) (n : ℕ) : G.SetConnGE S T n ↔ ↑n ≤ G.setConnectivity S T

@[simp]

theorem Graph.SetConnGE_zero {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.SetConnGE S T 0

theorem Graph.SetConnGE.anti_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {n m : ℕ} {S T : Set α} (hle : n ≤ m) (h : G.SetConnGE S T m) : G.SetConnGE S T n

theorem Graph.SetConnGE.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) : G.SetConnGE T S n

theorem Graph.setConnGE_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} : G.SetConnGE S T n ↔ G.SetConnGE T S n

theorem Graph.setConnGE_vertexSet_inter_left_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} : G.SetConnGE (G.vertexSet ∩ S) T n ↔ G.SetConnGE S T n

theorem Graph.SetConnGE.vertexSet_inter_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} : G.SetConnGE S T n → G.SetConnGE (G.vertexSet ∩ S) T n

Alias of the reverse direction of Graph.setConnGE_vertexSet_inter_left_iff.

theorem Graph.setConnGE_vertexSet_inter_right_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} : G.SetConnGE S (G.vertexSet ∩ T) n ↔ G.SetConnGE S T n

theorem Graph.SetConnGE.vertexSet_inter_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} : G.SetConnGE S T n → G.SetConnGE S (G.vertexSet ∩ T) n

Alias of the reverse direction of Graph.setConnGE_vertexSet_inter_right_iff.

@[simp]

theorem Graph.setConnGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.SetConnGE S T 1 ↔ G.SetConnected S T

theorem Graph.SetConnGE.SetConnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) (hn : n ≠ 0) : G.SetConnected S T

theorem Graph.SetConnGE.exists_isPathFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) (hn : n ≠ 0) : ∃ (P : WList α β), G.IsPathFrom S T P

theorem Graph.SetConnGE.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) (X : Set α) : (G.deleteVerts X).SetConnGE S T (↑n - (X ∩ G.vertexSet).encard).toNat

theorem Graph.SetConnGE.deleteVerts' {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) (X : Set α) : (G.deleteVerts X).SetConnGE (S \ X) (T \ X) (↑n - (X ∩ G.vertexSet).encard).toNat

theorem Graph.SetConnGE.subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S S' T T' : Set α} (h : G.SetConnGE S T n) (hS : S ⊆ S') (hT : T ⊆ T') : G.SetConnGE S' T' n

theorem Graph.setConnGE_inter_ncard {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (hFin : (G.vertexSet ∩ S ∩ T).Finite) : G.SetConnGE S T (G.vertexSet ∩ S ∩ T).ncard

theorem Graph.SetConnGE.left_encard_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) : ↑n ≤ (G.vertexSet ∩ S).encard

theorem Graph.SetConnGE.right_encard_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (h : G.SetConnGE S T n) : ↑n ≤ (G.vertexSet ∩ T).encard

theorem Graph.SetConnGE.subset_of_left_bound {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnGE S T S.ncard) (hS : S.Finite) : S ⊆ G.vertexSet

theorem Graph.SetConnGE.subset_of_right_bound {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (h : G.SetConnGE S T T.ncard) (hT : T.Finite) : T ⊆ G.vertexSet

theorem Graph.SetConnGE.left_bound_anti {α : Type u_1} {β : Type u_2} {G : Graph α β} {U S T : Set α} (hS : S.Finite) (h : G.SetConnGE S T S.ncard) (hU : U ⊆ S) : G.SetConnGE U T U.ncard

theorem Graph.SetConnGE.right_bound_anti {α : Type u_1} {β : Type u_2} {G : Graph α β} {U S T : Set α} (hT : T.Finite) (h : G.SetConnGE S T T.ncard) (hU : U ⊆ T) : G.SetConnGE S U U.ncard

theorem Graph.setConnGE_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : S.Finite) (hsu : S ⊆ G.vertexSet) : G.SetConnGE S S S.ncard

def Graph.EdgeSetConnGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) (n : ℕ) : Prop

Equations

• G.EdgeSetConnGE S T n = ∀ ⦃F : Set β⦄, G.IsEdgeSetCut S T F → ↑n ≤ F.encard

noncomputable def Graph.edgeSetConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : ℕ∞

Minimum F.encard over edge set cuts F between S and T, as an ℕ∞.

Equations

• G.edgeSetConnectivity S T = ⨅ (F : { F : Set β // G.IsEdgeSetCut S T F }), (↑F).encard

theorem Graph.le_edgeSetConnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} (S T : Set α) : k ≤ G.edgeSetConnectivity S T ↔ ∀ ⦃F : Set β⦄, G.IsEdgeSetCut S T F → k ≤ F.encard

theorem Graph.edgeSetConnGE_iff_le_edgeSetConnectivity {α : Type u_1} {β : Type u_2} {G : Graph α β} (S T : Set α) (n : ℕ) : G.EdgeSetConnGE S T n ↔ ↑n ≤ G.edgeSetConnectivity S T

@[simp]

theorem Graph.EdgeSetConnGE_zero {α : Type u_1} {β : Type u_2} (G : Graph α β) (S T : Set α) : G.EdgeSetConnGE S T 0

theorem Graph.EdgeSetConnGE.anti_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {n m : ℕ} {S T : Set α} (hle : n ≤ m) (h : G.EdgeSetConnGE S T m) : G.EdgeSetConnGE S T n

@[simp]

theorem Graph.EdgeSetConnGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} : G.EdgeSetConnGE S T 1 ↔ G.SetConnected S T

theorem Graph.EdgeSetConnGE.of_not_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {S T : Set α} (hdj : ¬Disjoint G.vertexSet (S ∩ T)) : G.EdgeSetConnGE S T n