eccent_eq_zero_iff — Mathlib

English

Let G be a simple graph with vertex set α. For any vertex u ∈ α, the eccentricity e(u) = G.eccent(u) is zero if and only if α is a subsingleton (has at most one element).

Русский

Пусть G — простой граф на множестве вершин α. Тогда эксцентриситет вершины u равен нулю тогда и только тогда, когда α является subsingleton (не более чем один элемент).

LaTeX

$$$G\mathrm{eccent}(u) = 0 \iff Subsingleton(\alpha)$$$

Lean4

theorem eccent_eq_zero_iff (u : α) : G.eccent u = 0 ↔ Subsingleton α :=
  by
  refine ⟨fun h ↦ ?_, fun _ ↦ eccent_eq_zero_of_subsingleton u⟩
  contrapose! h
  exact eccent_ne_zero u

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