le_minDegree_of_forall_le_degree — Mathlib

English

For any k, if k ≤ deg_G(v) for all vertices v, then k ≤ minDegree_G.

Русский

Для любого k, если k ≤ deg_G(v) для всех вершин v, то k ≤ minDegree_G.

LaTeX

$$∀ k, (∀ v, k ≤ G.degree v) → k ≤ G.minDegree$$

Lean4

/-- In a nonempty graph, if `k` is at most the degree of every vertex, it is at most the minimum
degree. Note the assumption that the graph is nonempty is necessary as long as `G.minDegree` is
defined to be a natural. -/
theorem le_minDegree_of_forall_le_degree [DecidableRel G.Adj] [Nonempty V] (k : ℕ) (h : ∀ v, k ≤ G.degree v) :
    k ≤ G.minDegree := by
  rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩
  rw [hv]
  apply h

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