Distance

noncomputable def Graph.eDist {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : ℕ∞

The number of edges of the shortest walk between two vertices x,y of G, as an ℕ∞. Equal to ⊤ if x and y are not ConnBetween in G, in particular if x = y ∉ V(G).

Equations

• G.eDist x y = ⨅ (W : { W : WList α β // G.IsWalk W ∧ W.first = x ∧ W.last = y }), ↑(↑W).length

theorem Graph.ConnBetween.eDist_lt_top {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.ConnBetween x y) : G.eDist x y < ⊤

theorem Graph.IsWalk.eDist_le_length {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) : G.eDist W.first W.last ≤ ↑W.length

theorem Graph.IsWalk.isPath_of_length_eq_eDist {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsWalk P) (hlen : ↑P.length = G.eDist P.first P.last) : G.IsPath P

theorem Graph.ConnBetween.exists_isPath_length_eq_eDist {α : 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 ∧ ↑P.length = G.eDist x y

The eDistance from x to y is realized by a path from x to y.

@[simp]

theorem Graph.eDist_lt_top_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.eDist x y < ⊤ ↔ G.ConnBetween x y

@[simp]

theorem Graph.eDist_eq_top_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.eDist x y = ⊤ ↔ ¬G.ConnBetween x y

theorem Graph.eDist_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} (x y : α) : G.eDist x y = G.eDist y x

theorem Graph.eDist_self {α : Type u_1} {β : Type u_2} {x : α} (G : Graph α β) (hx : x ∈ G.vertexSet) : G.eDist x x = 0

theorem Graph.eDist_self_eq_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.eDist x x = 0 ↔ x ∈ G.vertexSet

@[simp]

theorem Graph.eDist_eq_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : G.eDist x y = 0 ↔ x = y ∧ x ∈ G.vertexSet

theorem Graph.Adj.eDist_le_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.Adj x y) : G.eDist x y ≤ 1

theorem Graph.Adj.eDist_eq_one_of_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.Adj x y) (hne : x ≠ y) : G.eDist x y = 1

theorem Graph.eDist_triangle {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y z : α) : G.eDist x z ≤ G.eDist x y + G.eDist y z

theorem Graph.Adj.eDist_le_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.Adj x y) (z : α) : G.eDist x z ≤ G.eDist y z + 1

theorem Graph.ConnBetween.exists_adj_eDist_eq_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hconn : G.ConnBetween x y) (hne : x ≠ y) : ∃ (y' : α), G.Adj y' y ∧ G.eDist x y = G.eDist x y' + 1

If x and y are eDistinct vertices that are connected in G, then y has a neighbour y' whose eDistance to x is one less than that of y.

theorem Graph.exists_adj_of_eDist_eq_add_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {n : ℕ} (hxy : G.eDist x y = ↑n + 1) : ∃ (y' : α), G.Adj y' y ∧ G.eDist x y' = ↑n

ℕ - valued eDistance

noncomputable def Graph.dist {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : ℕ

Equations

• G.dist x y = (G.eDist x y).toNat

theorem Graph.dist_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : G.dist x y = G.dist y x

theorem Graph.ConnBetween.cast_dist {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hG : G.ConnBetween x y) : ↑(G.dist x y) = G.eDist x y

theorem Graph.Connected.cast_dist {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hG : G.Connected) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : ↑(G.dist x y) = G.eDist x y

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

theorem Graph.IsWalk.dist_le_length {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) : G.dist W.first W.last ≤ W.length

theorem Graph.dist_triangle {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hxy : G.ConnBetween x y) (z : α) : G.dist x z ≤ G.dist x y + G.dist y z

Shortest Paths

structure Graph.IsShortestPath {α : Type u_1} {β : Type u_2} (G : Graph α β) (P : WList α β) : Prop

G.IsShortestPath P means that P there is no walk of G between the ends of P with fewer edges than P itself.

• isPath : G.IsPath P
• length_eq_eDist : ↑P.length = G.eDist P.first P.last

theorem Graph.IsShortestPath.length_eq_dist {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsShortestPath P) : P.length = G.dist P.first P.last

theorem Graph.IsWalk.isShortestPath_of_length_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsWalk P) (heDist : P.length ≤ G.dist P.first P.last) : G.IsShortestPath P

theorem Graph.isShortestPath_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.IsShortestPath (WList.nil x)

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

theorem Graph.IsShortestPath.reverse {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsShortestPath P) : G.IsShortestPath P.reverse

@[simp]

theorem Graph.isShortestPath_reverse_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} : G.IsShortestPath P.reverse ↔ G.IsShortestPath P

@[simp]

theorem Graph.isShortestPath_nil_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.IsShortestPath (WList.nil x) ↔ x ∈ G.vertexSet

theorem Graph.IsShortestPath.prefix {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsShortestPath P) (hQ : Q.IsPrefix P) : G.IsShortestPath Q

theorem Graph.IsShortestPath.suffix {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsShortestPath P) (hQ : Q.IsSuffix P) : G.IsShortestPath Q

theorem Graph.IsShortestPath.sublist {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsShortestPath P) (hQ : Q.IsSublist P) : G.IsShortestPath Q