degree_le_maxDegree — Mathlib

English

For any vertex v, deg_G(v) ≤ maxDegree_G.

Русский

Для любой вершины v deg_G(v) ≤ maxDegree_G.

LaTeX

$$∀ v, deg_G(v) ≤ maxDegree(G)$$

Lean4

/-- The maximum degree in the graph is at least the degree of any particular vertex. -/
theorem degree_le_maxDegree [DecidableRel G.Adj] (v : V) : G.degree v ≤ G.maxDegree :=
  by
  obtain ⟨t, ht : _ = _⟩ := Finset.max_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))
  have := Finset.le_max_of_eq (mem_image_of_mem _ (mem_univ v)) ht
  rwa [maxDegree, ht, WithBot.unbotD_coe]

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