ediam_le_two_mul_radius — Mathlib

English

In finite graphs, the eccentric diameter is at most twice the radius.

Русский

Для конечных графов эдиям не превосходит вдвое радиуса.

LaTeX

$$$$ G.ediam \le 2 \cdot G.radius. $$$$

Lean4

theorem ediam_le_two_mul_radius [Finite α] : G.ediam ≤ 2 * G.radius :=
  by
  cases isEmpty_or_nonempty α
  · rw [radius_eq_top_of_isEmpty]
    exact le_top
  · by_cases h : G.Connected
    · obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
      obtain ⟨_, _, h⟩ := G.exists_edist_eq_ediam_of_ne_top (connected_iff_ediam_ne_top.mp h)
      apply le_trans (h ▸ G.edist_triangle (v := w))
      rw [two_mul]
      exact hw ▸ add_le_add (G.edist_comm ▸ G.edist_le_eccent) G.edist_le_eccent
    · rw [G.radius_eq_top_of_not_connected h]
      exact le_top

Похожие утверждения