minDegree — Mathlib

English

There exists a vertex with minimal degree: some v satisfies G.minDegree = G.degree(v).

Русский

Существует вершина, достигающая минимальную степень: существует v, такое что G.minDegree = G.degree(v).

LaTeX

$$∃ v, G.minDegree = G.degree v$$

Lean4

/-- The minimum degree of all vertices (and `0` if there are no vertices).
The key properties of this are given in `exists_minimal_degree_vertex`, `minDegree_le_degree`
and `le_minDegree_of_forall_le_degree`. -/
def minDegree [DecidableRel G.Adj] : ℕ :=
  WithTop.untopD 0 (univ.image fun v => G.degree v).min

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