feat(Combinatorics/SimpleGraph/Diam): add lemma eccent_eq_one_iff (leanprover-community#34085)

Author: IvanRenison

Mathlib/Combinatorics/SimpleGraph/Diam.lean

@@ -97,6 +97,27 @@ lemma eq_top_iff_forall_eccent_eq_one [Nontrivial α] :
   rw [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff.ne]
   exact huv.ne
 
+lemma eccent_le_iff (u : α) (k : ℕ∞) : G.eccent u ≤ k ↔ ∀ v, G.edist u v ≤ k :=
+  iSup_le_iff
+
+lemma eccent_le_one_iff (u : α) : G.eccent u ≤ 1 ↔ ∀ v, u ≠ v → G.Adj u v := by
+  constructor
+  · intro h v huv
+    have hd : G.edist u v ≤ 1 := LE.le.trans edist_le_eccent h
+    have hd' : 1 ≤ G.edist u v := Order.one_le_iff_pos.mpr (G.edist_pos_of_ne huv)
+    exact edist_eq_one_iff_adj.mp (le_antisymm (hd') hd).symm
+  · intro hall
+    rw [eccent_le_iff]
+    intro v
+    rw [edist_le_one_iff_adj_or_eq]
+    exact or_iff_not_imp_right.mpr (hall v)
+
+lemma eccent_eq_one_iff [Nontrivial α] (u : α) :
+    G.eccent u = 1 ↔ ∀ v, u ≠ v → G.Adj u v := by
+  have h : 1 ≤ G.eccent u := ENat.one_le_iff_ne_zero.mpr (eccent_ne_zero u)
+  rw [← LE.le.ge_iff_eq' h]
+  exact eccent_le_one_iff u
+
 end eccent
 
 section ediam

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -134,6 +134,14 @@ theorem edist_eq_one_iff_adj : G.edist u v = 1 ↔ G.Adj u v := by
     exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw
   · exact le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)
 
+lemma edist_le_one_iff_adj_or_eq : G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v := by
+  by_cases huv : u = v
+  · simp [huv]
+  · simp only [huv, or_false]
+    have h : 0 < G.edist u v := edist_pos_of_ne huv
+    rw [LE.le.ge_iff_eq' (Order.one_le_iff_pos.mpr h)]
+    exact edist_eq_one_iff_adj
+
 lemma edist_bot_of_ne (h : u ≠ v) : (⊥ : SimpleGraph V).edist u v = ⊤ := by
   rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h