theorem Graph.ConnBetween.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {x y : α} (f : α → α') (h : G.ConnBetween x y) : (Graph.map f G).ConnBetween (f x) (f y)

theorem Graph.Preconnected.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} (f : α → α') (h : G.Preconnected) : (Graph.map f G).Preconnected

@[simp]

theorem Graph.Connected.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} (f : α → α') (h : G.Connected) : (Graph.map f G).Connected

Pulling separators back along a map

theorem Graph.IsSep.of_map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {G : Graph α β} {f : α → α'} {S : Set α'} (hS : (map f G).IsSep S) : G.IsSep (G.vertexSet ∩ f ⁻¹' S)

theorem Graph.IsSep.of_contract {α : Type u_1} {β : Type u_3} {G : Graph α β} {S : Set α} {C : Set β} {φ : α → α} (hφ : (G.restrict C).connPartition.IsRepFun φ) (hS : G /[C, φ].IsSep S) : G.IsSep (φ ⁻¹' S)

Connectivity bounds under contracting a single edge

theorem Graph.ConnGE.contract_isLink {α : Type u_1} {β : Type u_3} {G : Graph α β} {x y : α} {e : β} {n : ℕ} (hG : G.ConnGE (n + 1)) (hl : G.IsLink e x y) : G /(e, hl).ConnGE n

Endpoint separators from bad single-edge contractions

If contracting a nonloop edge destroys ConnGE (n+1) (and the contracted graph still has at least n+2 vertices), then there is a separator in G of size at most n+1 containing both endpoints of the edge.

theorem Graph.ConnGE.exists_isSepSet_endpoints_of_not_connGE_contract_isLink {α : Type u_1} {β : Type u_3} {G : Graph α β} {x y : α} {e : β} {n : ℕ} (hG : G.ConnGE (n + 1)) (hl : G.IsLink e x y) (hnV : ↑n + 1 < G /(e, hl).vertexSet.encard) (hbad : ¬G /(e, hl).ConnGE (n + 1)) : ∃ (T : Set α), G.IsSep T ∧ T.encard ≤ ↑n + 1 ∧ x ∈ T ∧ y ∈ T

theorem Graph.exists_contract_connGE_three {α : Type u_1} {β : Type u_3} {G : Graph α β} [G.Finite] (hG : G.ConnGE 3) (hV : 5 ≤ G.vertexSet.encard) : ∃ (e : β) (x : α) (y : α) (h : G.IsLink e x y), G /(e, h).ConnGE 3