feat:(Combinatorics/SimpleGraph): connected SimpleGraph forms a MetricSpace

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -372,6 +372,15 @@ theorem reverse_reverse {u v : V} (p : G.Walk u v) : p.reverse.reverse = p := by
   | cons _ _ ih => simp [ih]
 #align simple_graph.walk.reverse_reverse SimpleGraph.Walk.reverse_reverse
 
+theorem reverse_surjective {u v : V} : Function.Surjective (reverse : G.Walk u v → _) :=
+  RightInverse.surjective reverse_reverse
+
+theorem reverse_injective {u v : V} : Function.Injective (reverse : G.Walk u v → _) :=
+  RightInverse.injective reverse_reverse
+
+theorem reverse_bijective {u v : V} : Function.Bijective (reverse : G.Walk u v → _) :=
+  And.intro reverse_injective reverse_surjective
+
 @[simp]
 theorem length_nil {u : V} : (nil : G.Walk u u).length = 0 := rfl
 #align simple_graph.walk.length_nil SimpleGraph.Walk.length_nil

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -1,32 +1,31 @@
 /-
 Copyright (c) 2022 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller, Vincent Beffara
+Authors: Kyle Miller, Vincent Beffara, Rida Hamadani
 -/
 import Mathlib.Combinatorics.SimpleGraph.Connectivity
-import Mathlib.Data.Nat.Lattice
+import Mathlib.Topology.MetricSpace.Basic
+import Mathlib.Data.ENat.Lattice
 
 #align_import combinatorics.simple_graph.metric from "leanprover-community/mathlib"@"352ecfe114946c903338006dd3287cb5a9955ff2"
 
 /-!
 # Graph metric
 
-This module defines the `SimpleGraph.dist` function, which takes
-pairs of vertices to the length of the shortest walk between them.
+This module defines the `SimpleGraph.edist` function, which takes pairs of vertices to the length of
+the shortest walk between them, or `⊤` if they are disconnected. It also defines `SimpleGraph.dist`
+which is the `ℕ`-valued version of `SimpleGraph.edist`.
 
 ## Main definitions
 
+- `SimpleGraph.edist` is the graph extended metric.
 - `SimpleGraph.dist` is the graph metric.
 
 ## Todo
 
 - Provide an additional computable version of `SimpleGraph.dist`
   for when `G` is connected.
 
-- Evaluate `Nat` vs `ENat` for the codomain of `dist`, or potentially
-  having an additional `edist` when the objects under consideration are
-  disconnected graphs.
-
 - When directed graphs exist, a directed notion of distance,
   likely `ENat`-valued.
 
@@ -39,109 +38,201 @@
 
 namespace SimpleGraph
 
+/-! ## Metric -/
+
+section edist
+
 variable {V : Type*} (G : SimpleGraph V)
 
-/-! ## Metric -/
+/--
+The extended distance between two vertices is the length of the shortest walk between them.
+It is `⊤` if no such walk exists.
+-/
+noncomputable def edist (u v : V) : ℕ∞ :=
+  ⨅ w : G.Walk u v, w.length
+
+variable {G} {u v w : V}
+
+theorem edist_eq_sInf : G.edist u v = sInf (Set.range fun w : G.Walk u v ↦ (w.length : ℕ∞)) := rfl
+
+protected theorem Reachable.exists_walk_length_eq_edist (hr : G.Reachable u v) :
+    ∃ p : G.Walk u v, p.length = G.edist u v :=
+  csInf_mem <| Set.range_nonempty_iff_nonempty.mpr hr
+
+protected theorem Connected.exists_walk_length_eq_edist  (hconn : G.Connected) (u v : V) :
+    ∃ p : G.Walk u v, p.length = G.edist u v :=
+  (hconn u v).exists_walk_length_eq_edist
+
+theorem edist_le (p : G.Walk u v) :
+    G.edist u v ≤ p.length :=
+  sInf_le ⟨p, rfl⟩
+protected alias Walk.edist_le := edist_le
+
+@[simp]
+theorem edist_eq_zero_iff :
+    G.edist u v = 0 ↔ u = v := by
+  apply Iff.intro <;> simp [edist, ENat.iInf_eq_zero]
+
+theorem edist_self : edist G v v = 0 :=
+  edist_eq_zero_iff.mpr rfl
+
+theorem edist_pos_of_ne (hne : u ≠ v) :
+    0 < G.edist u v :=
+  pos_iff_ne_zero.mpr <| edist_eq_zero_iff.ne.mpr hne
+
+lemma edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) :
+    G.edist u v = ⊤ := by
+  simp [edist, not_reachable_iff_isEmpty_walk.mp h]
+
+theorem reachable_of_edist_ne_top (h : G.edist u v ≠ ⊤) :
+    G.Reachable u v :=
+  not_not.mp <| edist_eq_top_of_not_reachable.mt h
+
+lemma exists_walk_of_edist_ne_top (h : G.edist u v ≠ ⊤) :
+    ∃ p : G.Walk u v, p.length = G.edist u v :=
+  (reachable_of_edist_ne_top h).exists_walk_length_eq_edist
+
+protected theorem edist_triangle : G.edist u w ≤ G.edist u v + G.edist v w := by
+  rcases eq_or_ne (G.edist u v) ⊤ with huv | huv
+  case inl => simp [huv]
+  case inr =>
+    rcases eq_or_ne (G.edist v w) ⊤ with hvw | hvw
+    case inl => simp [hvw]
+    case inr =>
+      obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
+      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
+      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
+      exact edist_le _
+
+theorem edist_comm : G.edist u v = G.edist v u := by
+  rw [edist_eq_sInf, ← Set.image_univ, ← Set.image_univ_of_surjective Walk.reverse_surjective,
+    ← Set.image_comp, Set.image_univ, Function.comp_def]
+  simp_rw [Walk.length_reverse, ← edist_eq_sInf]
+
+lemma exists_walk_of_edist_eq_coe {k : ℕ} (h : G.edist u v = k) :
+    ∃ p : G.Walk u v, p.length = k :=
+  have : G.edist u v ≠ ⊤ := by rw [h]; exact ENat.coe_ne_top _
+  have ⟨p, hp⟩ := exists_walk_of_edist_ne_top this
+  ⟨p, Nat.cast_injective (hp.trans h)⟩
+
+lemma edist_ne_top_iff_reachable : G.edist u v ≠ ⊤ ↔ G.Reachable u v := by
+  refine ⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩
+  by_contra hx
+  simp only [edist, iInf_eq_top, ENat.coe_ne_top] at hx
+  exact h.elim hx
+
+/--
+The extended distance between vertices is equal to `1` if and only if these vertices are adjacent.
+-/
+@[simp]
+theorem edist_eq_one_iff_adj : G.edist u v = 1 ↔ G.Adj u v := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp
+    exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw
+  · exact le_antisymm (edist_le h.toWalk) (ENat.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)
 
+end edist
 
-/-- The distance between two vertices is the length of the shortest walk between them.
-If no such walk exists, this uses the junk value of `0`. -/
+section dist
+
+variable {V : Type*} (G : SimpleGraph V)
+
+/--
+The distance between two vertices is the length of the shortest walk between them.
+If no such walk exists, this uses the junk value of `0`.
+-/
 noncomputable def dist (u v : V) : ℕ :=
-  sInf (Set.range (Walk.length : G.Walk u v → ℕ))
+  (G.edist u v).toNat
 #align simple_graph.dist SimpleGraph.dist
 
-variable {G}
+variable {G} {u v w : V}
 
-protected theorem Reachable.exists_walk_of_dist {u v : V} (hr : G.Reachable u v) :
+theorem dist_eq_sInf : G.dist u v = sInf (Set.range (Walk.length : G.Walk u v → ℕ)) :=
+  ENat.iInf_toNat
+
+protected theorem Reachable.exists_walk_length_eq_dist (hr : G.Reachable u v) :
     ∃ p : G.Walk u v, p.length = G.dist u v :=
-  Nat.sInf_mem (Set.range_nonempty_iff_nonempty.mpr hr)
-#align simple_graph.reachable.exists_walk_of_dist SimpleGraph.Reachable.exists_walk_of_dist
+  dist_eq_sInf ▸ Nat.sInf_mem (Set.range_nonempty_iff_nonempty.mpr hr)
+#align simple_graph.reachable.exists_walk_of_dist SimpleGraph.Reachable.exists_walk_length_eq_dist
 
-protected theorem Connected.exists_walk_of_dist (hconn : G.Connected) (u v : V) :
+protected theorem Connected.exists_walk_length_eq_dist (hconn : G.Connected) (u v : V) :
     ∃ p : G.Walk u v, p.length = G.dist u v :=
-  (hconn u v).exists_walk_of_dist
-#align simple_graph.connected.exists_walk_of_dist SimpleGraph.Connected.exists_walk_of_dist
+  dist_eq_sInf ▸ (hconn u v).exists_walk_length_eq_dist
+#align simple_graph.connected.exists_walk_of_dist SimpleGraph.Connected.exists_walk_length_eq_dist
 
-theorem dist_le {u v : V} (p : G.Walk u v) : G.dist u v ≤ p.length :=
-  Nat.sInf_le ⟨p, rfl⟩
+theorem dist_le (p : G.Walk u v) : G.dist u v ≤ p.length :=
+  dist_eq_sInf ▸ Nat.sInf_le ⟨p, rfl⟩
 #align simple_graph.dist_le SimpleGraph.dist_le
 
 @[simp]
-theorem dist_eq_zero_iff_eq_or_not_reachable {u v : V} :
-    G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v := by simp [dist, Nat.sInf_eq_zero, Reachable]
+theorem dist_eq_zero_iff_eq_or_not_reachable :
+    G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v := by simp [dist_eq_sInf, Nat.sInf_eq_zero, Reachable]
 #align simple_graph.dist_eq_zero_iff_eq_or_not_reachable SimpleGraph.dist_eq_zero_iff_eq_or_not_reachable
 
-theorem dist_self {v : V} : dist G v v = 0 := by simp
+theorem dist_self : dist G v v = 0 := by simp
 #align simple_graph.dist_self SimpleGraph.dist_self
 
-protected theorem Reachable.dist_eq_zero_iff {u v : V} (hr : G.Reachable u v) :
+protected theorem Reachable.dist_eq_zero_iff (hr : G.Reachable u v) :
     G.dist u v = 0 ↔ u = v := by simp [hr]
 #align simple_graph.reachable.dist_eq_zero_iff SimpleGraph.Reachable.dist_eq_zero_iff
 
-protected theorem Reachable.pos_dist_of_ne {u v : V} (h : G.Reachable u v) (hne : u ≠ v) :
+protected theorem Reachable.pos_dist_of_ne (h : G.Reachable u v) (hne : u ≠ v) :
     0 < G.dist u v :=
   Nat.pos_of_ne_zero (by simp [h, hne])
 #align simple_graph.reachable.pos_dist_of_ne SimpleGraph.Reachable.pos_dist_of_ne
 
-protected theorem Connected.dist_eq_zero_iff (hconn : G.Connected) {u v : V} :
+protected theorem Connected.dist_eq_zero_iff (hconn : G.Connected) :
     G.dist u v = 0 ↔ u = v := by simp [hconn u v]
 #align simple_graph.connected.dist_eq_zero_iff SimpleGraph.Connected.dist_eq_zero_iff
 
-protected theorem Connected.pos_dist_of_ne {u v : V} (hconn : G.Connected) (hne : u ≠ v) :
+protected theorem Connected.pos_dist_of_ne (hconn : G.Connected) (hne : u ≠ v) :
     0 < G.dist u v :=
-  Nat.pos_of_ne_zero (by intro h; exact False.elim (hne (hconn.dist_eq_zero_iff.mp h)))
+  Nat.pos_of_ne_zero fun h ↦ False.elim <| hne <| (hconn.dist_eq_zero_iff).mp h
 #align simple_graph.connected.pos_dist_of_ne SimpleGraph.Connected.pos_dist_of_ne
 
-theorem dist_eq_zero_of_not_reachable {u v : V} (h : ¬G.Reachable u v) : G.dist u v = 0 := by
+theorem dist_eq_zero_of_not_reachable (h : ¬G.Reachable u v) : G.dist u v = 0 := by
   simp [h]
 #align simple_graph.dist_eq_zero_of_not_reachable SimpleGraph.dist_eq_zero_of_not_reachable
 
-theorem nonempty_of_pos_dist {u v : V} (h : 0 < G.dist u v) :
+theorem nonempty_of_pos_dist (h : 0 < G.dist u v) :
     (Set.univ : Set (G.Walk u v)).Nonempty := by
+  rw [dist_eq_sInf] at h
   simpa [Set.range_nonempty_iff_nonempty, Set.nonempty_iff_univ_nonempty] using
     Nat.nonempty_of_pos_sInf h
 #align simple_graph.nonempty_of_pos_dist SimpleGraph.nonempty_of_pos_dist
 
-protected theorem Connected.dist_triangle (hconn : G.Connected) {u v w : V} :
+protected theorem Connected.dist_triangle (hconn : G.Connected) :
     G.dist u w ≤ G.dist u v + G.dist v w := by
-  obtain ⟨p, hp⟩ := hconn.exists_walk_of_dist u v
-  obtain ⟨q, hq⟩ := hconn.exists_walk_of_dist v w
+  obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v
+  obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w
   rw [← hp, ← hq, ← Walk.length_append]
   apply dist_le
 #align simple_graph.connected.dist_triangle SimpleGraph.Connected.dist_triangle
 
-private theorem dist_comm_aux {u v : V} (h : G.Reachable u v) : G.dist u v ≤ G.dist v u := by
-  obtain ⟨p, hp⟩ := h.symm.exists_walk_of_dist
-  rw [← hp, ← Walk.length_reverse]
-  apply dist_le
-
-theorem dist_comm {u v : V} : G.dist u v = G.dist v u := by
-  by_cases h : G.Reachable u v
-  · apply le_antisymm (dist_comm_aux h) (dist_comm_aux h.symm)
-  · have h' : ¬G.Reachable v u := fun h' => absurd h'.symm h
-    simp [h, h', dist_eq_zero_of_not_reachable]
+theorem dist_comm : G.dist u v = G.dist v u := by
+  rw [dist, dist, edist_comm]
 #align simple_graph.dist_comm SimpleGraph.dist_comm
 
-lemma dist_ne_zero_iff_ne_and_reachable {u v : V} : G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v := by
+lemma dist_ne_zero_iff_ne_and_reachable : G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v := by
   rw [ne_eq, dist_eq_zero_iff_eq_or_not_reachable.not]
   push_neg; rfl
 
-lemma Reachable.of_dist_ne_zero {u v : V} (h : G.dist u v ≠ 0) : G.Reachable u v :=
+lemma Reachable.of_dist_ne_zero (h : G.dist u v ≠ 0) : G.Reachable u v :=
   (dist_ne_zero_iff_ne_and_reachable.mp h).2
 
-lemma exists_walk_of_dist_ne_zero {u v : V} (h : G.dist u v ≠ 0) :
+lemma exists_walk_of_dist_ne_zero (h : G.dist u v ≠ 0) :
     ∃ p : G.Walk u v, p.length = G.dist u v :=
-  (Reachable.of_dist_ne_zero h).exists_walk_of_dist
+  (Reachable.of_dist_ne_zero h).exists_walk_length_eq_dist
 
-/- The distance between vertices is equal to `1` if and only if these vertices are adjacent. -/
-theorem dist_eq_one_iff_adj {u v : V} : G.dist u v = 1 ↔ G.Adj u v := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · let ⟨w, hw⟩ := exists_walk_of_dist_ne_zero <| ne_zero_of_eq_one h
-    exact w.adj_of_length_eq_one <| h ▸ hw
-  · have : h.toWalk.length = 1 := Walk.length_cons _ _
-    exact ge_antisymm (h.reachable.pos_dist_of_ne h.ne) (this ▸ dist_le _)
+/--
+The distance between vertices is equal to `1` if and only if these vertices are adjacent.
+-/
+@[simp]
+theorem dist_eq_one_iff_adj : G.dist u v = 1 ↔ G.Adj u v := by
+  rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]
+  decide
 
-theorem Walk.isPath_of_length_eq_dist {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) :
+theorem Walk.isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) :
     p.IsPath := by
   classical
   have : p.bypass = p := by
@@ -152,14 +243,38 @@
   rw [← this]
   apply Walk.bypass_isPath
 
-lemma Reachable.exists_path_of_dist {u v : V} (hr : G.Reachable u v) :
+lemma Reachable.exists_path_of_dist (hr : G.Reachable u v) :
     ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v := by
-  obtain ⟨p, h⟩ := hr.exists_walk_of_dist
+  obtain ⟨p, h⟩ := hr.exists_walk_length_eq_dist
   exact ⟨p, p.isPath_of_length_eq_dist h, h⟩
 
 lemma Connected.exists_path_of_dist (hconn : G.Connected) (u v : V) :
     ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v := by
-  obtain ⟨p, h⟩ := hconn.exists_walk_of_dist u v
+  obtain ⟨p, h⟩ := hconn.exists_walk_length_eq_dist  u v
   exact ⟨p, p.isPath_of_length_eq_dist h, h⟩
 
+end dist
+
+section Topology
+
+def Verts {V : Type*} (_ : SimpleGraph V) := V
+
+variable (V : Type*) (G : SimpleGraph V)
+
+noncomputable instance (h : Connected G) : MetricSpace (Verts G) where
+  dist x y := (G.dist x y : ℝ)
+  dist_self := by simp
+  dist_comm x y := by push_cast; norm_cast; exact dist_comm
+  dist_triangle x y z := by push_cast; norm_cast; exact h.dist_triangle
+  edist_dist x y := by push_cast; norm_cast
+  eq_of_dist_eq_zero := by
+    intro x y h
+    push_cast at h
+    rw [Nat.cast_eq_zero, dist_eq_zero_iff_eq_or_not_reachable] at h
+    cases h with
+    | inl => assumption
+    | inr h' => exfalso; exact h' <| h x y
+
+end Topology
+
 end SimpleGraph

Mathlib/Data/ENat/Lattice.lean

@@ -45,7 +45,23 @@ lemma coe_iSup : BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞)
 @[norm_cast] lemma coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) :=
   WithTop.coe_iInf (OrderBot.bddBelow _)
 
-variable {s : Set ℕ∞}
+@[simp]
+lemma iInf_eq_top_of_isEmpty [IsEmpty ι] : ⨅ i, (f i : ℕ∞) = ⊤ :=
+  iInf_coe_eq_top.mpr ‹_›
+
+lemma iInf_toNat : (⨅ i, (f i : ℕ∞)).toNat = ⨅ i, f i := by
+  cases isEmpty_or_nonempty ι
+  · simp
+  · norm_cast
+
+lemma iInf_eq_zero : ⨅ i, (f i : ℕ∞) = 0 ↔ ∃ i, f i = 0 := by
+  cases isEmpty_or_nonempty ι
+  · simp
+  · norm_cast
+    rw [iInf, Nat.sInf_eq_zero]
+    exact ⟨fun h ↦ by simp_all, .inl⟩
+
+variable {f : ι → ℕ∞} {s : Set ℕ∞}
 
 lemma sSup_eq_zero : sSup s = 0 ↔ ∀ a ∈ s, a = 0 :=
   sSup_eq_bot