maxDegree — Mathlib

English

Definition: The maximum degree is the largest degree among all vertices, with 0 as a lower bound if there are no vertices.

Русский

Определение: максимальная степень — наибольшая степень вершин; при отсутствии вершин минимальное значение равно 0.

LaTeX

$$maxDegree[G] = max_v deg_G(v) (with 0 as lower bound)$$

Lean4

/-- The maximum degree of all vertices (and `0` if there are no vertices).
The key properties of this are given in `exists_maximal_degree_vertex`, `degree_le_maxDegree`
and `maxDegree_le_of_forall_degree_le`. -/
def maxDegree [DecidableRel G.Adj] : ℕ :=
  WithBot.unbotD 0 (univ.image fun v => G.degree v).max

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