radius_bot — Mathlib

English

The radius of the edgeless graph on a nontrivial α is top (infinite).

Русский

Радиус графа без ребер на непустом α равен верхнему элементу (бесконечности).

LaTeX

$$$$ [\mathrmNontrivial(\alpha)] \Rightarrow (\perp : \mathrm{SimpleGraph}(\alpha)).radius = \top. $$$$

Lean4

@[simp]
theorem radius_bot [Nontrivial α] : (⊥ : SimpleGraph α).radius = ⊤ :=
  radius_eq_top_of_not_connected not_connected_bot

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