exists_minimal_degree_vertex — Mathlib

English

If a graph G is regular of degree d, then for every vertex v, G.degree(v) = d.

Русский

Если граф G регулярный степени d, то для каждой вершины v выполняется G.degree(v) = d.

LaTeX

$$∀ v, G.degree v = d$$

Lean4

/-- There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as
the lemma implies there exists a vertex. -/
theorem exists_minimal_degree_vertex [DecidableRel G.Adj] [Nonempty V] : ∃ v, G.minDegree = G.degree v :=
  by
  obtain ⟨t, ht : _ = _⟩ := min_of_nonempty (univ_nonempty.image fun v => G.degree v)
  obtain ⟨v, _, rfl⟩ := mem_image.mp (mem_of_min ht)
  exact ⟨v, by simp [minDegree, ht]⟩

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