@[simp]

theorem isLeast_empty {α : Type u_3} [LE α] {m : α} : ¬IsLeast ∅ m

theorem diff_nonempty_of_encard_lt_encard {α : Type u_1} {s t : Set α} (h : s.encard < t.encard) : (t \ s).Nonempty

theorem Graph.ConnBetween.walkable_eq_walkable {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.ConnBetween x y) : G.walkable x = G.walkable y

Connectivity on a graph

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

A graph is preconnected if for every pair of vertices, there is a path between them.

Equations

• G.Preconnected = ∀ (x y : α), x ∈ G.vertexSet → y ∈ G.vertexSet → G.ConnBetween x y

theorem Graph.Preconnected.isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.Preconnected) (hsle : H ≤s G) : G.Preconnected

@[simp]

theorem Graph.IsComplete.preconnected {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsComplete) : G.Preconnected

theorem Graph.preconnected_bot {α : Type u_1} {β : Type u_2} : ⊥.Preconnected

theorem Graph.preconnected_of_exists_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : ∃ (x : α), ∀ y ∈ G.vertexSet, G.ConnBetween x y) : G.Preconnected

theorem Graph.preconnected_iff_exists_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.Preconnected ↔ ∀ y ∈ G.vertexSet, G.ConnBetween x y

@[simp]

theorem Graph.preconnected_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_3} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Preconnected ↔ G.Preconnected

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

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

A graph is connected if it is a minimal closed subgraph of itself

Equations

• G.Connected = G.IsCompOf G

theorem Graph.Connected.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : G.vertexSet.Nonempty

@[simp]

theorem Graph.bot_not_connected {α : Type u_1} {β : Type u_2} : ¬⊥.Connected

theorem Graph.Connected.ne_bot {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : G ≠ ⊥

theorem Graph.connected_iff_forall_closed {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : G.Connected ↔ ∀ ⦃H : Graph α β⦄, H.IsClosedSubgraph G → H.vertexSet.Nonempty → H = G

theorem Graph.connected_iff_forall_closed_ge {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.vertexSet.Nonempty) : G.Connected ↔ ∀ ⦃H : Graph α β⦄, H.IsClosedSubgraph G → H.vertexSet.Nonempty → G ≤ H

theorem Graph.Connected.eq_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Connected) (hH : H.IsClosedSubgraph G) (hne : H.vertexSet.Nonempty) : H = G

theorem Graph.Connected.isSimpleOrder {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) (hnonempty : G ≠ ⊥) : IsSimpleOrder G.ClosedSubgraph

theorem Graph.IsClosedSubgraph.disjoint_or_subset_of_isCompOf {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : H.IsClosedSubgraph G) (hK : K.IsCompOf G) : K.IsCompOf H ∨ K.StronglyDisjoint H

theorem Graph.IsCompOf.of_le_le {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : K.IsCompOf G) (hKH : K ≤ H) (hHG : H ≤ G) : K.IsCompOf H

theorem Graph.ConnBetween.mem_walkable {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.ConnBetween x y) : y ∈ (G.walkable x).vertexSet

theorem Graph.connected_of_vertex {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) (h : ∀ y ∈ G.vertexSet, G.ConnBetween y u) : G.Connected

If G has one vertex connected to all others, then G is connected.

theorem Graph.connBetween_iff_mem_walkable_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.ConnBetween x y ↔ y ∈ (G.walkable x).vertexSet

theorem Graph.Connected.connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.Connected) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.ConnBetween x y

theorem Graph.Connected.pre {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) : G.Preconnected

theorem Graph.connected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected ↔ G.vertexSet.Nonempty ∧ G.Preconnected

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

@[simp]

theorem Graph.connected_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_3} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Connected ↔ G.Connected

theorem Graph.preconnected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Preconnected ↔ G = ⊥ ∨ G.Connected

theorem Graph.preconnected_iff_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.Preconnected ↔ G.Connected

theorem Graph.connected_of_exists_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : ∃ x ∈ G.vertexSet, ∀ y ∈ G.vertexSet, G.ConnBetween x y) : G.Connected

theorem Graph.connected_iff_exists_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.Connected ↔ ∀ y ∈ G.vertexSet, G.ConnBetween x y

theorem Graph.exists_not_connBetween_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : ¬G.Connected) (hx : x ∈ G.vertexSet) : ∃ y ∈ G.vertexSet, ¬G.ConnBetween x y

theorem Graph.Connected.of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.Connected) (hsle : H ≤s G) : G.Connected

theorem Graph.Preconnected.of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.Preconnected) (hsle : H ≤s G) : G.Preconnected

@[simp]

theorem Graph.IsComplete.connected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsComplete) : G.Connected ↔ G.vertexSet.Nonempty

theorem Graph.Preconnected.eq_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Preconnected) (hH : H.IsClosedSubgraph G) (hne : H.vertexSet.Nonempty) : H = G

theorem Graph.not_preconnected_of_ne_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsClosedSubgraph G) (hV₁ : H₁.vertexSet.Nonempty) (h₂ : H₂.IsClosedSubgraph G) (hV₂ : H₂.vertexSet.Nonempty) (hdj : H₁ ≠ H₂) : ¬G.Preconnected

Cut

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

A partition of G.V into two parts with no edge between them.

• left : Set α
• right : Set α
• nonempty_left : self.left.Nonempty
• nonempty_right : self.right.Nonempty
• disjoint : Disjoint self.left self.right
• union_eq : self.left ∪ self.right = G.vertexSet
• not_adj ⦃x y : α⦄ : x ∈ self.left → y ∈ self.right → ¬G.Adj x y

theorem Graph.Separation.left_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.left ⊆ G.vertexSet

theorem Graph.Separation.right_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.right ⊆ G.vertexSet

def Graph.Separation.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G.Separation

Equations

• S.symm = { left := S.right, right := S.left, nonempty_left := ⋯, nonempty_right := ⋯, disjoint := ⋯, union_eq := ⋯, not_adj := ⋯ }

@[simp]

theorem Graph.Separation.symm_left {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.symm.left = S.right

@[simp]

theorem Graph.Separation.symm_right {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.symm.right = S.left

@[simp]

theorem Graph.Separation.left_ssubset {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.left ⊂ G.vertexSet

@[simp]

theorem Graph.Separation.right_ssubset {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.right ⊂ G.vertexSet

@[simp]

theorem Graph.Separation.symm_symm {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : S.symm.symm = S

theorem Graph.Separation.not_left_mem_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (S : G.Separation) (hxV : x ∈ G.vertexSet) : x ∉ S.left ↔ x ∈ S.right

theorem Graph.Separation.not_right_mem_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (S : G.Separation) (hxV : x ∈ G.vertexSet) : x ∉ S.right ↔ x ∈ S.left

theorem Graph.Separation.left_mem_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {S : G.Separation} (hx : x ∈ S.left) (hxy : G.Adj x y) : y ∈ S.left

theorem Graph.Separation.right_mem_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {S : G.Separation} (hx : x ∈ S.right) (hxy : G.Adj x y) : y ∈ S.right

theorem Graph.Separation.mem_or_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (S : G.Separation) (hxV : x ∈ G.vertexSet) : x ∈ S.left ∨ x ∈ S.right

theorem Graph.Separation.edge_induce_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : Disjoint G[S.left].edgeSet G[S.right].edgeSet

theorem Graph.Separation.eq_union {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G = G[S.left] ∪ G[S.right]

theorem Graph.Separation.edge_mem_or_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (S : G.Separation) (he : e ∈ G.edgeSet) : e ∈ G[S.left].edgeSet ∨ e ∈ G[S.right].edgeSet

theorem Graph.Separation.vertexSet_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G.vertexSet.Nontrivial

theorem Graph.Separation.induce_left_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G[S.left].IsClosedSubgraph G

theorem Graph.Separation.induce_right_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G[S.right].IsClosedSubgraph G

def Graph.Separation.of_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : ¬G.ConnBetween x y) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G.Separation

Equations

• One or more equations did not get rendered due to their size.

theorem Graph.Separation.not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (S : G.Separation) (hx : x ∈ S.left) (hy : y ∈ S.right) : ¬G.ConnBetween x y

theorem Graph.Separation.isSepBetween_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {X : Set α} (S : (G.deleteVerts X).Separation) (hx : x ∈ S.left) (hy : y ∈ S.right) : G.IsSepBetween x y (G.vertexSet ∩ X)

theorem Graph.Separation.induce_stronglyDisjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G[S.left].StronglyDisjoint G[S.right]

theorem Graph.Separation.induce_left_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G[S.left] < G

theorem Graph.Separation.induce_right_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : G[S.right] < G

theorem Graph.exists_mem_left_of_nonempty_separation {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : Nonempty G.Separation) (hx : x ∈ G.vertexSet) : ∃ (S : G.Separation), x ∈ S.left

theorem Graph.exists_separation_of_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxV : x ∈ G.vertexSet) (hyV : y ∈ G.vertexSet) (hxy : ¬G.ConnBetween x y) : ∃ (S : G.Separation), x ∈ S.left ∧ y ∈ S.right

theorem Graph.preconnected_iff_isEmpty_separation {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Preconnected ↔ IsEmpty G.Separation

theorem Graph.Preconnected.separation_isEmpty {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Preconnected → IsEmpty G.Separation

Alias of the forward direction of Graph.preconnected_iff_isEmpty_separation.

theorem Graph.preconnected_of_vertexSet_subsingleton {α : Type u_1} {β : Type u_2} {G : Graph α β} (hV : G.vertexSet.Subsingleton) : G.Preconnected

theorem Graph.Separation.not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (S : G.Separation) : ¬G.Connected

theorem Graph.Connected.isEmpty_separation {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : IsEmpty G.Separation

theorem Graph.nonempty_separation_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (hne : G.vertexSet.Nonempty) (hG : ¬G.Connected) : Nonempty G.Separation

theorem Graph.not_connected_iff_nonempty_separation {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.vertexSet.Nonempty ∧ ¬G.Connected ↔ Nonempty G.Separation

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

G.IsSep S means that S is a subset of the vertices whose deletion leaves a disconnected graph

• subset_vx : S ⊆ G.vertexSet
• not_connected : ¬(G.deleteVerts S).Connected

theorem Graph.isSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : G.IsSep S ↔ S ⊆ G.vertexSet ∧ ¬(G.deleteVerts S).Connected

structure Graph.IsMinSep {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) extends G.IsSep S : Prop

• subset_vx : S ⊆ G.vertexSet
• not_connected : ¬(G.deleteVerts S).Connected
• minimal (A : Set α) : G.IsSep A → S.encard ≤ A.encard

theorem Graph.isMinSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) : G.IsMinSep S ↔ G.IsSep S ∧ ∀ (A : Set α), G.IsSep A → S.encard ≤ A.encard

theorem Graph.IsMinSep.encard_le_of_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (hS : G.IsMinSep S) (hT : G.IsSep T) : S.encard ≤ T.encard

theorem Graph.IsMinSep.not_isSep_of_encard_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' : Set α} (hM : G.IsMinSep S) (hSS' : S'.encard < S.encard) : ¬G.IsSep S'

theorem Graph.connected_of_not_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hV : S ⊆ G.vertexSet) (hS : ¬G.IsSep S) : (G.deleteVerts S).Connected

@[simp]

theorem Graph.empty_isSep_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsSep ∅ ↔ ¬G.Connected

theorem Graph.empty_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : ¬G.Connected) : G.IsSep ∅

theorem Graph.IsSep.not_connected_of_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsSep ∅) : ¬G.Connected

@[simp]

theorem Graph.IsMinSep.eq_empty_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : G.IsMinSep S) : S = ∅ ↔ ¬G.Connected

@[simp]

theorem Graph.empty_isMinSep_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsMinSep ∅ ↔ ¬G.Connected

theorem Graph.IsMinSep.connected_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hS : G.IsMinSep S) : G.Connected ↔ S.Nonempty

theorem Graph.IsMinSep.encard_eq_encard_of_isMinSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (hS : G.IsMinSep S) (hT : G.IsMinSep T) : S.encard = T.encard

theorem Graph.isSep_empty_iff_isMinSep_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsSep ∅ ↔ G.IsMinSep ∅

theorem Graph.conn_iff_forall_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected ↔ ∀ ⦃S : Set α⦄, G.IsSep S → S.Nonempty

theorem Graph.IsSep.nonempty_of_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hG : G.Connected) (hS : G.IsSep S) : S.Nonempty

theorem Graph.IsMinSep.nonempty_of_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (hG : G.Connected) (hM : G.IsMinSep S) : S.Nonempty

theorem Graph.vertexSet_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsSep G.vertexSet

theorem Graph.isSep_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (h : ¬(G.deleteVerts S).Connected) : G.IsSep (G.vertexSet ∩ S)

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

theorem Graph.IsSep.of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (h : G.IsSep S) (hsle : H ≤s G) : H.IsSep S

theorem Graph.IsComplete.isInducedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.IsComplete) (hH : H.IsInducedSubgraph G) : H.IsComplete

@[simp]

theorem Graph.IsComplete.isSep_iff_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} (h : G.IsComplete) : G.IsSep S ↔ S = G.vertexSet

theorem Graph.neighbor_isSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) (h : ∃ v ∈ G.vertexSet, v ≠ x ∧ ¬G.Adj x v) : G.IsSep (N(G, x) \ {x})

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

• subset_edgeSet : S ⊆ G.edgeSet
• not_connected : ¬(G.deleteEdges S).Connected

theorem Graph.isEdgeSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set β) : G.IsEdgeSep S ↔ S ⊆ G.edgeSet ∧ ¬(G.deleteEdges S).Connected

structure Graph.IsMinEdgeSep {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set β) extends G.IsEdgeSep S : Prop

• subset_edgeSet : S ⊆ G.edgeSet
• not_connected : ¬(G.deleteEdges S).Connected
• minimal (A : Set β) : G.IsEdgeSep A → S.encard ≤ A.encard

theorem Graph.isMinEdgeSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set β) : G.IsMinEdgeSep S ↔ G.IsEdgeSep S ∧ ∀ (A : Set β), G.IsEdgeSep A → S.encard ≤ A.encard

theorem Graph.IsMinEdgeSep.isEdgeSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hM : G.IsMinEdgeSep F) : G.IsEdgeSep F

theorem Graph.IsMinEdgeSep.encard_le_of_isEdgeSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {F F' : Set β} (hF : G.IsMinEdgeSep F) (hF' : G.IsEdgeSep F') : F.encard ≤ F'.encard

@[simp]

theorem Graph.empty_isEdgeSep_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsEdgeSep ∅ ↔ ¬G.Connected

structure Graph.IsMixedSep {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) (F : Set β) : Prop

• subset_vertexSet : S ⊆ G.vertexSet
• subset_edgeSet : F ⊆ G.edgeSet
• not_connected : ¬((G.deleteEdges F).deleteVerts S).Connected

theorem Graph.isMixedSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) (F : Set β) : G.IsMixedSep S F ↔ S ⊆ G.vertexSet ∧ F ⊆ G.edgeSet ∧ ¬((G.deleteEdges F).deleteVerts S).Connected

noncomputable def Graph.IsMixedSep.size {α : Type u_1} {β : Type u_2} (S : Set α) (F : Set β) : ℕ∞

Equations

• Graph.IsMixedSep.size S F = S.encard + F.encard

structure Graph.IsMinMixedSep {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) (F : Set β) extends G.IsMixedSep S F : Prop

• subset_vertexSet : S ⊆ G.vertexSet
• subset_edgeSet : F ⊆ G.edgeSet
• not_connected : ¬((G.deleteEdges F).deleteVerts S).Connected
• minimal (S' : Set α) (F' : Set β) : G.IsMixedSep S' F' → IsMixedSep.size S F ≤ IsMixedSep.size S' F'

theorem Graph.isMinMixedSep_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (S : Set α) (F : Set β) : G.IsMinMixedSep S F ↔ G.IsMixedSep S F ∧ ∀ (S' : Set α) (F' : Set β), G.IsMixedSep S' F' → IsMixedSep.size S F ≤ IsMixedSep.size S' F'

theorem Graph.IsMinMixedSep.isMixedSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} {F : Set β} (hM : G.IsMinMixedSep S F) : G.IsMixedSep S F

theorem Graph.IsMinMixedSep.size_le_of_isMixedSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {S S' : Set α} {F F' : Set β} (hM : G.IsMinMixedSep S F) (h : G.IsMixedSep S' F') : IsMixedSep.size S F ≤ IsMixedSep.size S' F'

theorem Graph.IsEdgeSep.toIsMixedSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (h : G.IsEdgeSep F) : G.IsMixedSep ∅ F

theorem Graph.IsMixedSep.of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} {F : Set β} (h : G.IsMixedSep S F) (hsle : H ≤s G) : H.IsMixedSep S (H.edgeSet ∩ F)

def Graph.PreconnGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (n : ℕ) : Prop

A graph has PreconnGE n, if for every pair of vertices s and t, there is no n-vertex cut between them. In the case of complete graphs, K_n, ∀ κ, K_n.PreconnGE κ.

Equations

• G.PreconnGE n = ∀ ⦃s t : α⦄, s ∈ G.vertexSet → t ∈ G.vertexSet → G.ConnBetweenGE s t n

structure Graph.ConnGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (n : ℕ) : Prop

A graph has ConnGE n, if every cut has size at least n and the number of vertices is at least n + 1.

• le_cut ⦃C : Set α⦄ : G.IsSep C → ↑n ≤ C.encard
• le_card : G.vertexSet.Subsingleton ∨ ↑n < G.vertexSet.encard

theorem Graph.connGE_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (n : ℕ) : G.ConnGE n ↔ (∀ ⦃C : Set α⦄, G.IsSep C → ↑n ≤ C.encard) ∧ (G.vertexSet.Subsingleton ∨ ↑n < G.vertexSet.encard)

theorem Graph.exists_isSepSet_encard_lt_of_not_connGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hnV : ↑n < G.vertexSet.encard) (h : ¬G.ConnGE n) : ∃ (C : Set α), G.IsSep C ∧ C.encard < ↑n

theorem Graph.exists_isSepSet_encard_le_of_not_connGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hnV : ↑n + 1 < G.vertexSet.encard) (h : ¬G.ConnGE (n + 1)) : ∃ (C : Set α), G.IsSep C ∧ C.encard ≤ ↑n

def Graph.EdgeConnGE {α : Type u_1} {β : Type u_2} (G : Graph α β) (n : ℕ) : Prop

A graph has EdgeConnGE n, if for every pair of vertices s and t, there is no n-edge cut between them.

Equations

• G.EdgeConnGE n = ∀ ⦃s t : α⦄, s ∈ G.vertexSet → t ∈ G.vertexSet → G.EdgeConnBetweenGE s t n

@[simp]

theorem Graph.PreconnGE_zero {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.PreconnGE 0

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

@[simp]

theorem Graph.preconnGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.PreconnGE 1 ↔ G.Preconnected

theorem Graph.preconnGE_iff_forall_connBetweenGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} : G.PreconnGE n ↔ ∀ ⦃s t : α⦄, s ∈ G.vertexSet → t ∈ G.vertexSet → G.ConnBetweenGE s t n

theorem Graph.preconnGE_iff_forall_preconnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} : G.PreconnGE n ↔ ∀ X ⊆ G.vertexSet, X.encard < ↑n → (G.deleteVerts X).Preconnected

theorem Graph.preconnGE_map_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).PreconnGE n ↔ G.PreconnGE n

@[simp]

theorem Graph.preconnGE_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {β' : Type u_3} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).PreconnGE n ↔ G.PreconnGE n

theorem Graph.PreconnGE.preconnected_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {X : Set α} (hG : G.PreconnGE n) (hX : X.encard < ↑n) : (G.deleteVerts X).Preconnected

theorem Graph.PreconnGE.encard_ge {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {X : Set α} (hG : G.PreconnGE n) (hX : ¬(G.deleteVerts X).Preconnected) : ↑n ≤ X.encard

theorem Graph.PreconnGE_two_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.PreconnGE 2 ↔ G.Preconnected ∧ ∀ x ∈ G.vertexSet, (G.deleteVerts {x}).Preconnected

theorem Graph.preconnGE_iff_forall_setConnGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} : G.PreconnGE n ↔ ∀ (S T : Set α), S ⊆ G.vertexSet → T ⊆ G.vertexSet → G.SetConnGE S T (min (↑n) (min S.encard T.encard)).toNat

noncomputable def Graph.sepConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Minimum C.encard over vertex cuts C of G, as an ℕ∞.

Equations

• G.sepConnectivity = ⨅ (C : { C : Set α // G.IsSep C }), (↑C).encard

noncomputable def Graph.cardConnectivityBound {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Upper bound on connectivity from the vertex count: ⊤ if V(G) is a subsingleton, else |V(G)| - 1 in ℕ∞.

Equations

• G.cardConnectivityBound = if x : G.vertexSet.Subsingleton then ⊤ else G.vertexSet.encard - 1

noncomputable def Graph.connectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Global vertex connectivity as an ℕ∞: minimum of separator connectivity and the cardinality bound that appears in ConnGE.

Equations

• κ(G) = min G.sepConnectivity G.cardConnectivityBound

def Graph.«termκ(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Graph.preconnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Minimum pairwise connBetweenConnectivity over ordered pairs of vertices in V(G).

Equations

• κ'(G) = ⨅ (s : ↑G.vertexSet), ⨅ (t : ↑G.vertexSet), G.connectivityBetween ↑s ↑t

def Graph.«termκ'(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Graph.edgeConnectivity {α : Type u_1} {β : Type u_2} (G : Graph α β) : ℕ∞

Minimum pairwise edgeConnBetweenConnectivity over ordered pairs of vertices in V(G).

Equations

• κₑ(G) = ⨅ (s : ↑G.vertexSet), ⨅ (t : ↑G.vertexSet), G.edgeConnectivityBetween ↑s ↑t

def Graph.«termκₑ(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Graph.le_sepConnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} : k ≤ G.sepConnectivity ↔ ∀ ⦃C : Set α⦄, G.IsSep C → k ≤ C.encard

theorem Graph.nat_le_cardConnectivityBound_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (n : ℕ) : ↑n ≤ G.cardConnectivityBound ↔ G.vertexSet.Subsingleton ∨ ↑n < G.vertexSet.encard

theorem Graph.connGE_iff_le_connectivity {α : Type u_1} {β : Type u_2} {G : Graph α β} (n : ℕ) : G.ConnGE n ↔ ↑n ≤ κ(G)

theorem Graph.le_preconnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} : k ≤ κ'(G) ↔ ∀ ⦃s t : α⦄, s ∈ G.vertexSet → t ∈ G.vertexSet → k ≤ G.connectivityBetween s t

theorem Graph.preconnGE_iff_le_preconnectivity {α : Type u_1} {β : Type u_2} {G : Graph α β} (n : ℕ) : G.PreconnGE n ↔ ↑n ≤ κ'(G)

theorem Graph.le_edgeConnectivity_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} : k ≤ κₑ(G) ↔ ∀ ⦃s t : α⦄, s ∈ G.vertexSet → t ∈ G.vertexSet → k ≤ G.edgeConnectivityBetween s t

theorem Graph.connectivity_simplify {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) : κ(G) = κ(H)

theorem Graph.edgeConnGE_iff_le_edgeConnectivity {α : Type u_1} {β : Type u_2} {G : Graph α β} (n : ℕ) : G.EdgeConnGE n ↔ ↑n ≤ κₑ(G)

theorem Graph.PreconnGE.isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {n : ℕ} (hconn : H.PreconnGE n) (hsle : H ≤s G) : G.PreconnGE n

@[simp]

theorem Graph.IsComplete.preconnGE {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsComplete) (n : ℕ) : G.PreconnGE n

theorem Graph.encard_le_preconnGE_of_not_isComplete {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : ¬G.IsComplete) (hn : G.PreconnGE n) : ↑n ≤ G.vertexSet.encard

theorem Graph.preconnGE_add_two_le_encard_of_not_isComplete {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : ¬G.IsComplete) (hn : G.PreconnGE n) : ↑n + 2 ≤ G.vertexSet.encard

@[simp]

theorem Graph.connGE_zero {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.ConnGE 0

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

@[simp]

theorem Graph.connGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.ConnGE 1 ↔ G.Connected

@[simp]

theorem Graph.connGE_bot {α : Type u_1} {β : Type u_2} {n : ℕ} : ⊥.ConnGE n ↔ n = 0

@[simp]

theorem Graph.bouquet_deleteVerts {α : Type u_1} {β : Type u_2} {v : α} {F : Set β} : (bouquet v F).deleteVerts {v} = ⊥

@[simp]

theorem Graph.connGE_bouquet_iff {α : Type u_1} {β : Type u_2} {v : α} {F : Set β} (n : ℕ) : (bouquet v F).ConnGE n ↔ n ≤ 1

theorem Graph.connGE_iff_of_vertexSet_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {n : ℕ} (h : G.vertexSet = {x}) : G.ConnGE n ↔ n ≤ 1

theorem Graph.connGE_iff_of_vertexSet_subsingleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hss : G.vertexSet.Subsingleton) : G.ConnGE n ↔ ↑n ≤ G.vertexSet.encard

theorem Graph.ConnGE.pre {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : G.ConnGE n) : G.PreconnGE n

theorem Graph.preconnGE_iff_connGE_of_not_isComplete {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h' : G.vertexSet.encard ≤ ↑n → ¬G.IsComplete) : G.PreconnGE n ↔ G.ConnGE n

G.PreconnGE n and G.ConnGE n agree except on complete graphs on more than n vertices.

theorem Graph.connGE_iff_preconnGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hnt : G.vertexSet.Nontrivial) : G.ConnGE n ↔ G.PreconnGE n ∧ ↑n < G.vertexSet.encard

theorem Graph.preconnGE_iff_connGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} : G.PreconnGE n ↔ G.ConnGE n ∨ G.vertexSet.encard ≤ ↑n ∧ G.IsComplete

theorem Graph.connGE_iff_forall_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h' : G.vertexSet.encard = ↑n → ¬G.IsComplete) : G.ConnGE n ↔ ∀ X ⊆ G.vertexSet, X.encard < ↑n → (G.deleteVerts X).Connected

theorem Graph.connGE_map_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).ConnGE n ↔ G.ConnGE n

@[simp]

theorem Graph.connGE_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {β' : Type u_3} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).ConnGE n ↔ G.ConnGE n

theorem Graph.IsComplete.connGE_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsComplete) (n : ℕ) : G.ConnGE n ↔ G.vertexSet.Subsingleton ∧ ↑n ≤ G.vertexSet.encard ∨ ↑n < G.vertexSet.encard

theorem Graph.IsComplete.connGE_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsComplete) (n : ℕ) : G.ConnGE n ↔ G.vertexSet.Subsingleton ∧ ↑n = G.vertexSet.encard ∨ ↑n < G.vertexSet.encard

theorem Graph.IsComplete.connGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : G.IsComplete) (hn : ↑n < G.vertexSet.encard) : G.ConnGE n

theorem Graph.ConnGE.isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {n : ℕ} (h : H.ConnGE n) (hsle : H ≤s G) : G.ConnGE n

theorem Graph.ConnGE.of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {F : Set β} (h : (G.deleteEdges F).ConnGE n) : G.ConnGE n

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

theorem Graph.ConnGE.vertexSet_encard_of_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : G.ConnGE n) (hnt : G.vertexSet.Nontrivial) : ↑n + 1 ≤ G.vertexSet.encard

theorem Graph.ConnGE.lt_encard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hG : G.ConnGE n) (hn : 2 ≤ n) : ↑n < G.vertexSet.encard

A 2-connected graph has more than n vertices. This is the le_card field of ConnGE with the V(G).Subsingleton alternative ruled out: a subsingleton graph is ⊥ or a bouquet, and connGE_bot and connGE_bouquet_iff cap both at ConnGE 1.

theorem Graph.PreconnGE.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {X : Set α} (hX : X.Finite) (h : G.PreconnGE (n + hX.toFinset.card)) : (G.deleteVerts X).PreconnGE n

theorem Graph.ConnGE.deleteVerts' {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} {X : Set α} (hX : X.Finite) (h : G.ConnGE (n + hX.toFinset.card)) : (G.deleteVerts X).ConnGE n

theorem Graph.connGE_delete_vertex_of_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hG : G.ConnGE (n + 1)) (x : α) : (G.deleteVerts {x}).ConnGE n

theorem Graph.ConnGE.deleteVert_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hG : G.ConnGE 2) (hx : x ∈ G.vertexSet) : (G.deleteVerts {x}).Connected

theorem Graph.preconnGE_delete_vertex_of_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hG : G.PreconnGE (n + 1)) (x : α) : (G.deleteVerts {x}).PreconnGE n

theorem Graph.PreconnGE.preconnGE_add_one_of_delete_of_forall_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {n : ℕ} (hG : (G.deleteVerts {v}).PreconnGE n) (hv : ∀ x ∈ G.vertexSet, x ≠ v → G.Adj x v) : G.PreconnGE (n + 1)

If v is adjacent to every other vertex, then deleting it drops the preconnectivity by one.

theorem Graph.ConnGE.connGE_add_one_of_delete_of_forall_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} {n : ℕ} (hG : (G.deleteVerts {v}).ConnGE n) (hV : 3 ≤ G.vertexSet.encard) (hv : ∀ x ∈ G.vertexSet, x ≠ v → G.Adj x v) : G.ConnGE (n + 1)

If v is adjacent to every other vertex, then deleting it drops the connectivity by one.

@[simp]

theorem Graph.EdgeConnGE_zero {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.EdgeConnGE 0

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

@[simp]

theorem Graph.edgeConnGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.EdgeConnGE 1 ↔ G.Preconnected