ediam_eq_top — Mathlib

English

The diameter is top exactly when for every finite bound b, there exist two vertices with distance greater than b.

Русский

Диаметр равен верхней границе тогда и только тогда, когда для каждого конечного b существуют вершины u,v такие, что b < edist u v.

LaTeX

$$G.ediam = ⊤ ∧ ∀ b < ⊤, ∃ u v, b < G.edist u v$$

Lean4

theorem ediam_eq_top : G.ediam = ⊤ ↔ ∀ b < ⊤, ∃ u v, b < G.edist u v := by
  simp only [ediam, eccent, iSup_eq_top, lt_iSup_iff]

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