center — Mathlib

English

The center of a simple graph is the set of vertices whose eccentricity equals the radius.

Русский

Центр простого графа — это множество вершин, чья эксцентриситет равен радиусу.

LaTeX

$$$$ \mathrm{center}(G) = \{u \in \alpha \mid \mathrm{eccent}(u) = \mathrm{radius}(G)\}. $$$$

Lean4

/-- The center of a simple graph is the set of vertices with eccentricity equal to the radius. -/
def center (G : SimpleGraph α) : Set α :=
  {u | G.eccent u = G.radius}

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