maxDegree_lt_card_verts — Mathlib

English

If the vertex set V is nonempty, the maximum degree of G is strictly less than the number of vertices: maxDegree(G) < |V|.

Русский

Если множество вершин не пусто, то максимальная степень графа меньше числа вершин: maxDegree(G) < |V|.

LaTeX

$$$\\text{If } V \\neq \\varnothing:\\; \\maxDegree(G) < \\lvert V \\rvert$$$

Lean4

/-- The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption
that `V` is nonempty is necessary, as otherwise this would assert the existence of a
natural number less than zero. -/
theorem maxDegree_lt_card_verts [DecidableRel G.Adj] [Nonempty V] : G.maxDegree < Fintype.card V :=
  by
  obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
  rw [hv]
  apply G.degree_lt_card_verts v

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