exists_edist_eq_eccent_of_finite — Mathlib

English

If the vertex set is finite, then for every vertex u there exists a vertex v with distance equal to the eccentricity of u.

Русский

Если множество вершин конечное, для любой вершины u существует вершина v с расстоянием равным ecc(u).

LaTeX

$$∃v, G.edist u v = G.eccent u$$

Lean4

theorem exists_edist_eq_eccent_of_finite [Finite α] (u : α) : ∃ v, G.edist u v = G.eccent u :=
  have : Nonempty α := Nonempty.intro u
  exists_eq_ciSup_of_finite

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