Reachable and Connected

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

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

Equations

• G.Reachable x y = Nonempty (G.Walk x y)

theorem Graph.reachable_iff_nonempty_univ {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.Reachable x y ↔ Set.univ.Nonempty

theorem Graph.not_reachable_iff_isEmpty_walk {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : ¬G.Reachable x y ↔ IsEmpty (G.Walk x y)

theorem Graph.Reachable.elim {α : Type u_1} {β : Type u_2} {G : Graph α β} {p : Prop} {x y : α} (h : G.Reachable x y) (hp : ∀ (a : G.Walk x y), p) : p

theorem Graph.Walk.reachable {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (p : G.Walk x y) : G.Reachable x y

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

theorem Graph.Reachable.refl {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : G.Reachable x x

@[simp]

theorem Graph.Reachable.rfl {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.Reachable x x

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

theorem Graph.reachable_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.Reachable x y ↔ G.Reachable y x

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

theorem Graph.reachable_is_equivalence {α : Type u_1} {β : Type u_2} (G : Graph α β) : Equivalence G.Reachable

def Graph.reachableSetoid {α : Type u_1} {β : Type u_2} (G : Graph α β) : Setoid α

The equivalence relation on vertices given by Graph.Reachable.

Equations

• G.reachableSetoid = { r := G.Reachable, iseqv := ⋯ }

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

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

Equations

• G.Preconnected = ∀ (x y : ↑G.vertexSet), G.Reachable ↑x ↑y

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

A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.

• preconnected : G.Preconnected
• nonempty : Nonempty ↑G.vertexSet

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