minDegree_le_degree — Mathlib

English

For every vertex v, the minimum degree is less than or equal to its degree.

Русский

Для каждой вершины v минимальная степень не превосходит ее степени.

LaTeX

$$G.minDegree ≤ G.degree v$$

Lean4

/-- The minimum degree in the graph is at most the degree of any particular vertex. -/
theorem minDegree_le_degree [DecidableRel G.Adj] (v : V) : G.minDegree ≤ G.degree v :=
  by
  obtain ⟨t, ht⟩ := Finset.min_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))
  have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht
  rwa [minDegree, ht]

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