minDegree_le_maxDegree — Mathlib

English

The minimum degree is at most the maximum degree: minDegree ≤ maxDegree.

Русский

Минимальная степень не превышает максимальную: minDegree ≤ maxDegree.

LaTeX

$$minDegree(G) ≤ maxDegree(G)$$

Lean4

@[simp]
theorem minDegree_le_maxDegree [DecidableRel G.Adj] : G.minDegree ≤ G.maxDegree :=
  by
  by_cases he : IsEmpty V
  · simp
  · push_neg at he
    exact he.elim fun v ↦ (minDegree_le_degree _ v).trans (degree_le_maxDegree _ v)

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