Connectivity for general graphs

inductive UnweightedGraph.Walk {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} : α → α → 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 : UnweightedGraph α β} {u : α} : Walk u u
• cons {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} {u v w : α} (h : G.Adj u v) (p : Walk v w) : Walk u w

def UnweightedGraph.instDecidableEqWalk.decEq {α✝ : Type u_3} {β✝ : Type u_4} {G✝ : UnweightedGraph α✝ β✝} {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.
• UnweightedGraph.instDecidableEqWalk.decEq UnweightedGraph.Walk.nil UnweightedGraph.Walk.nil = isTrue ⋯
• UnweightedGraph.instDecidableEqWalk.decEq UnweightedGraph.Walk.nil (UnweightedGraph.Walk.cons h p) = isFalse ⋯
• UnweightedGraph.instDecidableEqWalk.decEq (UnweightedGraph.Walk.cons h p) UnweightedGraph.Walk.nil = isFalse ⋯

@[implicit_reducible]

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

Equations

• UnweightedGraph.instDecidableEqWalk = UnweightedGraph.instDecidableEqWalk.decEq

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

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

Equations

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

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

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

Equations

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

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

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

• preconnected : Preconnected
• nonempty : Nonempty α

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

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

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

Equations

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

def UnweightedGraph.vertexBoundary {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} (S : Set α) : Set α

We can define the vertex boundary δS of S to be the set of all vertices v not in S but adjacent to some vertex in S.

Equations

• UnweightedGraph.vertexBoundary S = {v : α | v ∉ S ∧ ∃ (u : ↑S) (e : ↑G.edgeSet), G.IsLink (↑e) (↑u) v}

theorem UnweightedGraph.walk_crossing {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [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 UnweightedGraph.connected_non_empty_edge_boundary {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [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 ≠ ∅.