maxDegree_le_of_forall_degree_le — Mathlib

English

If k is at least every vertex degree, then maxDegree ≤ k.

Русский

Если k не меньше степеней всех вершин, то maxDegree ≤ k.

LaTeX

$$maxDegree[G] ≤ k$$

Lean4

/-- In a graph, if `k` is at least the degree of every vertex, then it is at least the maximum
degree. -/
theorem maxDegree_le_of_forall_degree_le [DecidableRel G.Adj] (k : ℕ) (h : ∀ v, G.degree v ≤ k) : G.maxDegree ≤ k :=
  by
  by_cases hV : IsEmpty V
  · simp
  · push_neg at hV
    obtain ⟨_, hv⟩ := G.exists_maximal_degree_vertex
    exact hv ▸ h _

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