radius_ne_top_iff — Mathlib

English

For a finite nonempty vertex set, the radius is finite if and only if the graph is connected.

Русский

Для конечного непустого множества вершин радиус конечен тогда и только тогда граф связан.

LaTeX

$$$$\forall \alpha, \forall G:\mathrm{SimpleGraph}(\alpha), [\mathrm{Nonempty}(\alpha)] [\mathrm{Finite}(\alpha)]: \ G.radius \neq \top \iff G.\mathrm{Connected}. $$$$

Lean4

theorem radius_ne_top_iff [Nonempty α] [Finite α] : G.radius ≠ ⊤ ↔ G.Connected :=
  by
  refine ⟨Not.imp_symm radius_eq_top_of_not_connected, fun h ↦ ?_⟩
  obtain ⟨u, v, huv⟩ := G.exists_edist_eq_radius_of_finite
  rw [← huv, edist_ne_top_iff_reachable]
  exact h u v

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