connected_iff_diam_ne_zero — Mathlib

English

A finite and nontrivial graph is connected if and only if its diameter is not zero.

Русский

Конечный непустой граф связен тогда и только тогда, когда его диаметр не равен нулю.

LaTeX

$$$$ G.Connected \\iff G.diam \\neq 0 $$$$

Lean4

/-- A finite and nontrivial graph is connected if and only if its diameter is not zero.
See also `connected_iff_ediam_ne_top` for the extended diameter version. -/
theorem connected_iff_diam_ne_zero [Finite α] [Nontrivial α] : G.Connected ↔ G.diam ≠ 0 := by
  rw [connected_iff_ediam_ne_top, not_iff_not, diam_eq_zero_iff_ediam_eq_top]

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