Connectivity between two vertices

def Graph.ConnBetween {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : Prop

Equations

• G.ConnBetween x y = ∃ (w : WList α β), G.IsWalk w ∧ w.first = x ∧ w.last = y

theorem Graph.ConnBetween.refl {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.ConnBetween x x

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

instance Graph.instSymmConnBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} : Std.Symm G.ConnBetween

theorem Graph.connBetween_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.ConnBetween x y ↔ G.ConnBetween y x

theorem Graph.ConnBetween.left_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.ConnBetween x y) : x ∈ G.vertexSet

theorem Graph.ConnBetween.right_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.ConnBetween x y) : y ∈ G.vertexSet

theorem Graph.ConnBetween.trans {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y z : α} (hxy : G.ConnBetween x y) (hyz : G.ConnBetween y z) : G.ConnBetween x z

instance Graph.instIsTransConnBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} : IsTrans α G.ConnBetween

@[simp]

theorem Graph.connBetween_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.ConnBetween x x ↔ x ∈ G.vertexSet

theorem Graph.Adj.connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.Adj x y) : G.ConnBetween x y

theorem Graph.connBetween_eq_transGen {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.ConnBetween = Relation.TransGen fun (x y : α) => x = y ∧ x ∈ G.vertexSet ∨ G.Adj x y

theorem Graph.IsLink.connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : G.ConnBetween x y

theorem Graph.ConnBetween.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} (hle : H ≤ G) (h : H.ConnBetween x y) : G.ConnBetween x y

theorem Graph.ConnBetween.exists_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.ConnBetween x y) : ∃ (P : WList α β), G.IsPath P ∧ P.first = x ∧ P.last = y

theorem Graph.connBetween_iff_exists_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.ConnBetween x y ↔ ∃ (P : WList α β), G.IsPath P ∧ P.first = x ∧ P.last = y

@[simp]

theorem Graph.not_connBetween_of_left_not_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hx : x ∉ G.vertexSet) : ¬G.ConnBetween x y

@[simp]

theorem Graph.not_connBetween_of_right_not_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hy : y ∉ G.vertexSet) : ¬G.ConnBetween x y

theorem Graph.IsWalk.connBetween_of_mem_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {W : WList α β} (hW : G.IsWalk W) (hx : x ∈ W) (hy : y ∈ W) : G.ConnBetween x y

theorem Graph.IsWalk.connBetween_first_last {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) : G.ConnBetween W.first W.last

theorem Graph.connBetween_induce_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {X : Set α} (hx : x ∈ G.vertexSet) : G[X].ConnBetween x y ↔ ∃ (P : WList α β), G.IsPath P ∧ P.first = x ∧ P.last = y ∧ P.vertexSet ⊆ X

theorem Graph.IsComplete.connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : G.IsComplete) (hs : s ∈ G.vertexSet) (ht : t ∈ G.vertexSet) : G.ConnBetween s t

theorem Graph.ConnBetween.isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} (h : G.ConnBetween x y) (hle : H.IsClosedSubgraph G) (hx : x ∈ H.vertexSet) : H.ConnBetween x y

theorem Graph.connBetween_iff_of_edgeless {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.edgeSet = ∅) : G.ConnBetween x y ↔ x ∈ G.vertexSet ∧ x = y

theorem Graph.Isolated.connBetween_iff_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hisol : G.Isolated x) : G.ConnBetween x y ↔ x = y

theorem Graph.connBetween_iff_reflTransGen_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.ConnBetween x y ↔ x ∈ G.vertexSet ∧ Relation.ReflTransGen G.Adj x y

theorem Graph.connBetween_map_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {α' : Type u_5} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : (map φ G).ConnBetween (φ x) (φ y) ↔ G.ConnBetween x y

theorem Graph.connBetween_map_iff_of_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {α' : Type u_5} {φ : α → α'} (hφ : Function.Injective φ) : (map φ G).ConnBetween (φ x) (φ y) ↔ G.ConnBetween x y

@[simp]

theorem Graph.connBetween_edgeMap_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_5} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} {x y : α} : (G.edgeMap φ hφ).ConnBetween x y ↔ G.ConnBetween x y

Separators between two vertices

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

• subset : C ⊆ G.vertexSet
• left_not_mem : s ∉ C
• right_not_mem : t ∉ C
• not_connBetween : ¬(G.deleteVerts C).ConnBetween s t

theorem Graph.IsSepBetween.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {X : Set α} (hX : G.IsSepBetween s t X) : G.IsSepBetween t s X

instance Graph.instSymmIsSepBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} : Std.Symm fun (x1 x2 : α) => G.IsSepBetween x1 x2 X

theorem Graph.not_isSepBetween_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : α} {X : Set α} (hs : s ∈ G.vertexSet) : ¬G.IsSepBetween s s X

theorem Graph.IsLink.not_isSepBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {e : β} {X : Set α} (he : G.IsLink e s t) : ¬G.IsSepBetween s t X

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

theorem Graph.isSepBetween_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : ¬G.ConnBetween s t) : G.IsSepBetween s t ∅

theorem Graph.IsSepBetween.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s t : α} {X : Set α} (hX : G.IsSepBetween s t X) (hle : H ≤ G) : H.IsSepBetween s t (H.vertexSet ∩ X)

theorem Graph.IsWalk.not_disjoint_isSepBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {W : WList α β} (hW : G.IsWalk W) (hX : G.IsSepBetween W.first W.last X) : ¬Disjoint W.vertexSet X

theorem Graph.IsWalk.exists_mem_isSepBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {W : WList α β} (hW : G.IsWalk W) (hX : G.IsSepBetween W.first W.last X) : ∃ x ∈ W.vertexSet, x ∈ X

theorem Graph.IsComplete.not_isSepBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {X : Set α} (h : G.IsComplete) (hs : s ∈ G.vertexSet) (ht : t ∈ G.vertexSet) : ¬G.IsSepBetween s t X

theorem Graph.isSepBetween_of_not_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (hne : s ≠ t) (hnst : ¬G.Adj s t) : G.IsSepBetween s t (G.vertexSet \ {s, t})

theorem Graph.isSepBetween_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {X : Set α} (h : ¬(G.deleteVerts X).ConnBetween s t) (hs : s ∉ X) (ht : t ∉ X) : G.IsSepBetween s t (G.vertexSet ∩ X)

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

• subset_edgeSet : F ⊆ G.edgeSet
• not_connBetween : ¬(G.deleteEdges F).ConnBetween s t

theorem Graph.isEdgeCutBetween_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (s t : α) : G.IsEdgeCutBetween F s t ↔ F ⊆ G.edgeSet ∧ ¬(G.deleteEdges F).ConnBetween s t

theorem Graph.not_isEdgeCutBetween_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : α} {F : Set β} (hs : s ∈ G.vertexSet) : ¬G.IsEdgeCutBetween F s s

theorem Graph.isEdgeCutBetween_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : ¬G.ConnBetween s t) : G.IsEdgeCutBetween ∅ s t

theorem Graph.IsEdgeCutBetween.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {s t : α} {F : Set β} (hF : G.IsEdgeCutBetween F s t) (hle : H ≤ G) : H.IsEdgeCutBetween (H.edgeSet ∩ F) s t

theorem Graph.IsWalk.not_disjoint_isEdgeCutBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {W : WList α β} (hW : G.IsWalk W) (hF : G.IsEdgeCutBetween F W.first W.last) : ¬Disjoint W.edgeSet F

theorem Graph.IsWalk.exists_mem_isEdgeCutBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {W : WList α β} (hW : G.IsWalk W) (hF : G.IsEdgeCutBetween F W.first W.last) : ∃ e ∈ W.edgeSet, e ∈ F

Ensemble of paths between two vertices

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

Equations

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

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

• f : ι → WList α β
• isPath (i : ι) : G.IsPath (self.f i)
• first_eq (i : ι) : (self.f i).first = s
• last_eq (i : ι) : (self.f i).last = t

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

• f : ι → WList α β
• isPath (i : ι) : G.IsPath (self.f i)
• first_eq (i : ι) : (self.f i).first = s
• last_eq (i : ι) : (self.f i).last = t
• internallyDisjoint : Graph.internallyDisjoint s t self.f

def Graph.VertexEnsemble.edgeDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) : Prop

Equations

• P.edgeDisjoint = Pairwise (Function.onFun (Function.onFun Disjoint WList.edgeSet) P.f)

theorem Graph.VertexEnsemble.eq_or_eq_of_mem {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t x : α} {i j : ι} (P : G.VertexEnsemble s t ι) (hxi : x ∈ (P.f i).vertexSet) (hxj : x ∈ (P.f j).vertexSet) (hne : i ≠ j) : x = s ∨ x = t

@[simp]

theorem Graph.VertexEnsemble.ends_subset {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (i : ι) : {s, t} ⊆ (P.f i).vertexSet

@[simp]

theorem Graph.VertexEnsemble.vertexSet_inter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) {i j : ι} (hne : i ≠ j) : (P.f i).vertexSet ∩ (P.f j).vertexSet = {s, t}

theorem Graph.VertexEnsemble.nonempty_of_ne {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (hne : s ≠ t) (i : ι) : (P.f i).Nonempty

theorem Graph.VertexEnsemble.nontrivial_of_not_adj {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (hne : s ≠ t) (hadj : ¬G.Adj s t) (i : ι) : (P.f i).Nontrivial

def Graph.vertexEnsemble_empty {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (ι : Type u_5) [h : IsEmpty ι] : G.VertexEnsemble s t ι

Equations

• G.vertexEnsemble_empty s t ι = { f := fun (x : ι) => WList.nil s, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.vertexEnsemble_empty_f {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (ι : Type u_5) [h : IsEmpty ι] (x✝ : ι) : (G.vertexEnsemble_empty s t ι).f x✝ = WList.nil s

@[simp]

theorem Graph.vertexEnsemble_empty_edgeDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} [h : IsEmpty ι] : (G.vertexEnsemble_empty s t ι).edgeDisjoint

def Graph.vertexEnsemble_nil {α : Type u_1} {β : Type u_2} {s : α} (G : Graph α β) (h : s ∈ G.vertexSet) (ι : Type u_5) : G.VertexEnsemble s s ι

Equations

• G.vertexEnsemble_nil h ι = { f := fun (x : ι) => WList.nil s, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.vertexEnsemble_nil_f {α : Type u_1} {β : Type u_2} {s : α} (G : Graph α β) (h : s ∈ G.vertexSet) (ι : Type u_5) (x✝ : ι) : (G.vertexEnsemble_nil h ι).f x✝ = WList.nil s

@[simp]

theorem Graph.vertexEnsemble_nil_edgeDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s : α} (h : s ∈ G.vertexSet) : (G.vertexEnsemble_nil h ι).edgeDisjoint

def Graph.IsLink.vertexEnsemble {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {e : β} (ι : Type u_5) (h : G.IsLink e s t) (hne : s ≠ t) : G.VertexEnsemble s t ι

Equations

• Graph.IsLink.vertexEnsemble ι h hne = { f := fun (x : ι) => WList.cons s e (WList.nil t), isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.IsLink.vertexEnsemble_f {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {e : β} (ι : Type u_5) (h : G.IsLink e s t) (hne : s ≠ t) (x✝ : ι) : (vertexEnsemble ι h hne).f x✝ = WList.cons s e (WList.nil t)

def Graph.IsPath.vertexEnsemble {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : G.VertexEnsemble P.first P.last PUnit.{u_5 + 1}

Equations

• h.vertexEnsemble = { f := fun (x : PUnit.{?u.1 + 1}) => P, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.IsPath.vertexEnsemble_f {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) (x✝ : PUnit.{u_5 + 1}) : h.vertexEnsemble.f x✝ = P

@[simp]

theorem Graph.IsPath.vertexEnsemble_edgeDisjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : h.vertexEnsemble.edgeDisjoint

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

Equations

• P.comp f = { f := P.f ∘ ⇑f, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.VertexEnsemble.comp_f {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (f : ι' ↪ ι) (a✝ : ι') : (P.comp f).f a✝ = (P.f ∘ ⇑f) a✝

@[simp]

theorem Graph.VertexEnsemble.comp_edgeDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} {P : G.VertexEnsemble s t ι} (hP : P.edgeDisjoint) (f : ι' ↪ ι) : (P.comp f).edgeDisjoint

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

Equations

• P.of_le hle = { f := P.f, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.VertexEnsemble.of_le_f {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G H : Graph α β} {s t : α} (P : H.VertexEnsemble s t ι) (hle : H ≤ G) (a✝ : ι) : (P.of_le hle).f a✝ = P.f a✝

@[simp]

theorem Graph.VertexEnsemble.of_le_edgeDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G H : Graph α β} {s t : α} {P : H.VertexEnsemble s t ι} (hP : P.edgeDisjoint) (hle : H ≤ G) : (P.of_le hle).edgeDisjoint

def Graph.VertexEnsemble.vertexSet {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) : Set α

internal vertex set of a vertex ensemble

Equations

• P.vertexSet = (⋃ (i : ι), (P.f i).vertexSet) \ {s, t}

theorem Graph.VertexEnsemble.subset_vertexSet_of_mem {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (i : ι) : (P.f i).vertexSet \ {s, t} ⊆ P.vertexSet

def Graph.VertexEnsemble.sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (Q : G.VertexEnsemble s t ι') (h : Disjoint P.vertexSet Q.vertexSet) : G.VertexEnsemble s t (ι ⊕ ι')

Equations

• P.sum Q h = { f := fun (i : ι ⊕ ι') => Sum.elim P.f Q.f i, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, internallyDisjoint := ⋯ }

@[simp]

theorem Graph.VertexEnsemble.sum_f {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (Q : G.VertexEnsemble s t ι') (h : Disjoint P.vertexSet Q.vertexSet) (i : ι ⊕ ι') : (P.sum Q h).f i = Sum.elim P.f Q.f i

Ensemble of edge-disjoint paths between two vertices

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

An indexed family of s–t paths whose edge sets are pairwise disjoint.

• f : ι → WList α β
• isPath (i : ι) : G.IsPath (self.f i)
• first_eq (i : ι) : (self.f i).first = s
• last_eq (i : ι) : (self.f i).last = t
• edgeDisjoint : Pairwise (Function.onFun (Function.onFun Disjoint WList.edgeSet) self.f)

def Graph.edgePathEnsemble_empty {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (ι : Type u_5) [h : IsEmpty ι] : G.EdgePathEnsemble s t ι

Equations

• G.edgePathEnsemble_empty s t ι = { f := fun (x : ι) => h.elim x, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

@[simp]

theorem Graph.edgePathEnsemble_empty_f {α : Type u_1} {β : Type u_2} (G : Graph α β) (s t : α) (ι : Type u_5) [h : IsEmpty ι] (x✝ : ι) : (G.edgePathEnsemble_empty s t ι).f x✝ = h.elim x✝

def Graph.edgePathEnsemble_nil {α : Type u_1} {β : Type u_2} {s : α} (G : Graph α β) (h : s ∈ G.vertexSet) (ι : Type u_5) : G.EdgePathEnsemble s s ι

Equations

• G.edgePathEnsemble_nil h ι = { f := fun (x : ι) => WList.nil s, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

@[simp]

theorem Graph.edgePathEnsemble_nil_f {α : Type u_1} {β : Type u_2} {s : α} (G : Graph α β) (h : s ∈ G.vertexSet) (ι : Type u_5) (x✝ : ι) : (G.edgePathEnsemble_nil h ι).f x✝ = WList.nil s

def Graph.IsPath.edgePathEnsemble {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) : G.EdgePathEnsemble P.first P.last PUnit.{u_5 + 1}

Equations

• h.edgePathEnsemble = { f := fun (x : PUnit.{?u.1 + 1}) => P, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

@[simp]

theorem Graph.IsPath.edgePathEnsemble_f {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (h : G.IsPath P) (x✝ : PUnit.{u_5 + 1}) : h.edgePathEnsemble.f x✝ = P

def Graph.EdgePathEnsemble.comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} (P : G.EdgePathEnsemble s t ι) (g : ι' ↪ ι) : G.EdgePathEnsemble s t ι'

Equations

• P.comp g = { f := P.f ∘ ⇑g, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

@[simp]

theorem Graph.EdgePathEnsemble.comp_f {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} {s t : α} (P : G.EdgePathEnsemble s t ι) (g : ι' ↪ ι) (a✝ : ι') : (P.comp g).f a✝ = (P.f ∘ ⇑g) a✝

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

Equations

• P.of_le hle = { f := P.f, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

@[simp]

theorem Graph.EdgePathEnsemble.of_le_f {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G H : Graph α β} {s t : α} (P : H.EdgePathEnsemble s t ι) (hle : H ≤ G) (a✝ : ι) : (P.of_le hle).f a✝ = P.f a✝

def Graph.EdgePathEnsemble.ofVertexEnsemble {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} {s t : α} (P : G.VertexEnsemble s t ι) (h : {i : ι | ¬(P.f i).Nontrivial}.Subsingleton) : G.EdgePathEnsemble s t ι

Equations

• Graph.EdgePathEnsemble.ofVertexEnsemble P h = { f := P.f, isPath := ⋯, first_eq := ⋯, last_eq := ⋯, edgeDisjoint := ⋯ }

k-connectivity between two vertices

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

Equations

• G.ConnBetweenGE s t n = ∀ ⦃C : Set α⦄, G.IsSepBetween s t C → ↑n ≤ C.encard

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

Minimum C.encard over vertex separators C between s and t, as an ℕ∞.

Equations

• G.connectivityBetween s t = ⨅ (C : { C : Set α // G.IsSepBetween s t C }), (↑C).encard

theorem Graph.le_connectivityBetween_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} (s t : α) : k ≤ G.connectivityBetween s t ↔ ∀ ⦃C : Set α⦄, G.IsSepBetween s t C → k ≤ C.encard

theorem Graph.connBetweenGE_iff_le_connectivityBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} (s t : α) (n : ℕ) : G.ConnBetweenGE s t n ↔ ↑n ≤ G.connectivityBetween s t

@[simp]

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

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

theorem Graph.ConnBetweenGE.symm {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) : G.ConnBetweenGE t s n

instance Graph.instSymmConnBetweenGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} : Std.Symm fun (x1 x2 : α) => G.ConnBetweenGE x1 x2 n

theorem Graph.connBetweenGE_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} : G.ConnBetweenGE s t n ↔ G.ConnBetweenGE t s n

@[simp]

theorem Graph.connBetweenGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} : G.ConnBetweenGE s t 1 ↔ G.ConnBetween s t

theorem Graph.ConnBetweenGE.left_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hn : n ≠ 0) : s ∈ G.vertexSet

theorem Graph.ConnBetweenGE.right_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hn : n ≠ 0) : t ∈ G.vertexSet

@[simp]

theorem Graph.connBetweenGE_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : α} (hs : s ∈ G.vertexSet) (n : ℕ) : G.ConnBetweenGE s s n

theorem Graph.IsLink.connBetweenGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {e : β} (h : G.IsLink e s t) (n : ℕ) : G.ConnBetweenGE s t n

theorem Graph.Adj.connBetweenGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : G.Adj s t) (n : ℕ) : G.ConnBetweenGE s t n

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

theorem Graph.IsComplete.connBetweenGE {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} (h : G.IsComplete) (hs : s ∈ G.vertexSet) (ht : t ∈ G.vertexSet) (n : ℕ) : G.ConnBetweenGE s t n

theorem Graph.connBetweenGE_le_diff_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hne : s ≠ t) (hadj : ¬G.Adj s t) : ↑n ≤ (G.vertexSet \ {s, t}).encard

theorem Graph.connBetweenGE_le_encard_sub_two {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hne : s ≠ t) (hadj : ¬G.Adj s t) : ↑n ≤ G.vertexSet.encard - 2

theorem Graph.connBetweenGE_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hne : s ≠ t) (hadj : ¬G.Adj s t) : ↑n ≤ G.vertexSet.encard

theorem Graph.connBetweenGE_add_two_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} {n : ℕ} (h : G.ConnBetweenGE s t n) (hs : s ∈ G.vertexSet) (ht : t ∈ G.vertexSet) (hne : s ≠ t) (hadj : ¬G.Adj s t) : ↑n + 2 ≤ G.vertexSet.encard

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

Equations

• G.EdgeConnBetweenGE s t n = ∀ ⦃F : Set β⦄, G.IsEdgeCutBetween F s t → ↑n ≤ F.encard

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

Minimum F.encard over edge cuts F between s and t, as an ℕ∞.

Equations

• G.edgeConnectivityBetween s t = ⨅ (F : { F : Set β // G.IsEdgeCutBetween F s t }), (↑F).encard

theorem Graph.le_edgeConnectivityBetween_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ∞} (s t : α) : k ≤ G.edgeConnectivityBetween s t ↔ ∀ ⦃F : Set β⦄, G.IsEdgeCutBetween F s t → k ≤ F.encard

theorem Graph.edgeConnBetweenGE_iff_le_edgeConnectivityBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} (s t : α) (n : ℕ) : G.EdgeConnBetweenGE s t n ↔ ↑n ≤ G.edgeConnectivityBetween s t

@[simp]

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

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

theorem Graph.edgeConnBetweenGE_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {s t : α} : G.EdgeConnBetweenGE s t 1 ↔ G.ConnBetween s t

@[simp]

theorem Graph.edgeConnBetweenGE_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : α} (hs : s ∈ G.vertexSet) (n : ℕ) : G.EdgeConnBetweenGE s s n

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