nontrivial_of_diam_ne_zero — Mathlib

English

If diam ≠ 0, then the vertex set is nontrivial (exists two distinct vertices).

Русский

Если diam ≠ 0, то множество вершин не тривиально (существуют две различные вершины).

LaTeX

$$$$ G.diam \\neq 0 \\Rightarrow \\exists x,y \\in \\alpha, x \\neq y $$$$

Lean4

theorem nontrivial_of_diam_ne_zero (h : G.diam ≠ 0) : Nontrivial α :=
  by
  apply G.nontrivial_of_ediam_ne_zero
  contrapose! h
  simp [diam, h]

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