eccent_pos_iff — Mathlib

English

For any vertex u in α, the eccentricity e(u) is positive if and only if α is nontrivial (has at least two elements).

Русский

Для любой вершины u из α эксцентриситет e(u) положителен тогда и только тогда, когда α не тривиален (минимум два элемента).

LaTeX

$$$0 < G\mathrm{eccent}(u) \iff Nontrivial(\alpha)$$$

Lean4

theorem eccent_pos_iff (u : α) : 0 < G.eccent u ↔ Nontrivial α := by
  rw [pos_iff_ne_zero, ← not_subsingleton_iff_nontrivial, ← eccent_eq_zero_iff]

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