exists_eccent_eq_ediam_of_ne_top — Mathlib

English

There exists a vertex u with eccent(u) = ediam, provided α is nonempty and ediam ≠ ⊤.

Русский

Существует вершина u такая, что eccent(u) = ediam, при условии, что α непустой и ediam ≠ ⊤.

LaTeX

$$$ [Nonempty \\alpha] (h : G.ediam \\neq \\top) \\Rightarrow \\exists u, G.eccent u = G.ediam $$$

Lean4

theorem exists_eccent_eq_ediam_of_ne_top [Nonempty α] (h : G.ediam ≠ ⊤) : ∃ u, G.eccent u = G.ediam :=
  ENat.exists_eq_iSup_of_lt_top h.lt_top

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