exists_dist_eq_diam — Mathlib

English

There exist vertices u,v such that dist(u,v) = diam(G).

Русский

Существуют вершины u,v такие, что dist(u,v) = diam(G).

LaTeX

$$$$ \\exists u,v \\in \\alpha: G.dist(u,v) = G.diam $$$$

Lean4

theorem exists_dist_eq_diam [Nonempty α] : ∃ u v, G.dist u v = G.diam :=
  by
  by_cases h : G.diam = 0
  · simp [h]
  · obtain ⟨u, v, huv⟩ := exists_edist_eq_ediam_of_ne_top <| ediam_ne_top_of_diam_ne_zero h
    use u, v
    rw [diam, dist, congrArg ENat.toNat huv]

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