exists_maximal_degree_vertex — Mathlib

English

There exists a vertex of maximal degree: ∃ v, G.maxDegree = G.degree v.

Русский

Существует вершина максимальной степени: существует v such that G.maxDegree = G.degree v.

LaTeX

$$∃ v, G.maxDegree = G.degree v$$

Lean4

/-- There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as
the lemma implies there exists a vertex. -/
theorem exists_maximal_degree_vertex [DecidableRel G.Adj] [Nonempty V] : ∃ v, G.maxDegree = G.degree v :=
  by
  obtain ⟨t, ht⟩ := max_of_nonempty (univ_nonempty.image fun v => G.degree v)
  have ht₂ := mem_of_max ht
  simp only [mem_image, mem_univ, true_and] at ht₂
  rcases ht₂ with ⟨v, rfl⟩
  refine ⟨v, ?_⟩
  rw [maxDegree, ht, WithBot.unbotD_coe]

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