Connectivity for general graphs

inductive WeightedGraph.Walk {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} : α → α → Type u_1

A walk is a sequence of adjacent vertices. For vertices u v : α, the type Walk G u v consists of all walks starting at u and ending at v.

• nil {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} {u : α} : Walk u u
• cons {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} {u v w : α} (h : G.Adj u v) (p : Walk v w) : Walk u w

@[implicit_reducible]

instance WeightedGraph.instDecidableEqWalk {α✝ : Type u_3} {β✝ : Type u_4} {G✝ : WeightedGraph α✝ β✝} {a✝ a✝¹ : α✝} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (Walk a✝ a✝¹)

Equations

• WeightedGraph.instDecidableEqWalk = WeightedGraph.instDecidableEqWalk.decEq

def WeightedGraph.instDecidableEqWalk.decEq {α✝ : Type u_3} {β✝ : Type u_4} {G✝ : WeightedGraph α✝ β✝} {a✝ a✝¹ : α✝} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : Walk a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• WeightedGraph.instDecidableEqWalk.decEq WeightedGraph.Walk.nil WeightedGraph.Walk.nil = isTrue ⋯
• WeightedGraph.instDecidableEqWalk.decEq WeightedGraph.Walk.nil (WeightedGraph.Walk.cons h p) = isFalse ⋯
• WeightedGraph.instDecidableEqWalk.decEq (WeightedGraph.Walk.cons h p) WeightedGraph.Walk.nil = isFalse ⋯

def WeightedGraph.Reachable {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (u v : α) : Prop

Two vertices are reachable if there is a walk between them.

Equations

• WeightedGraph.Reachable u v = Nonempty (WeightedGraph.Walk u v)

def WeightedGraph.Preconnected {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} : Prop

A graph is preconnected if every pair of vertices is reachable from one another.

Equations

• WeightedGraph.Preconnected = ∀ (u v : α), WeightedGraph.Reachable u v

structure WeightedGraph.Connected {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} : Prop

A graph is connected if it's preconnected and contains at least one vertex.

• preconnected : Preconnected
• nonempty : Nonempty α

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

def WeightedGraph.edgeBoundary {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (S : Set α) : Set β

We define the edge boundary ∂S of S to consist of all edges with exactly one endpoint in S.

Equations

• WeightedGraph.edgeBoundary S = {e : β | e ∈ G.edgeSet ∧ ∃ a ∈ S, ∃ b ∈ Sᶜ, G.IsLink e a b}

theorem WeightedGraph.walk_crossing {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hβ : G.edgeSet = Set.univ) (S : Set α) {u v : α} (hW : Walk u v) : u ∈ S → v ∉ S → ∃ (e : β), e ∈ edgeBoundary S

If there is a walk going from S to Sᶜ then there is a least on edge that goes from S to Sᶜ.

theorem WeightedGraph.connected_non_empty_edge_boundary {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hβ : G.edgeSet = Set.univ) (h : Connected) (S : Set α) (hS_nonempty : S.Nonempty) (hS_ne_univ : S ≠ Set.univ) : Nonempty ↑(edgeBoundary S)

In a connected graph, every set of vertices, different from ∅ and univ, has non empty edgeBoundary: ∂S ≠ ∅.