radius_eq_top_of_isEmpty — Mathlib

English

If α is empty, then for any simple graph G on α we have radius(G) = ∞ (top).

Русский

Пусть α пустое; для любого простого графа G на α радиус G равен бесконечности (верхняя граница).

LaTeX

$$$$ \forall \alpha, \forall G:\mathrm{SimpleGraph}(\alpha), [\mathrm{IsEmpty}(\alpha)] \Rightarrow \mathrm{radius}(G) = \top. $$$$

Lean4

theorem radius_eq_top_of_isEmpty [IsEmpty α] : G.radius = ⊤ :=
  iInf_of_empty G.eccent

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