Theorems · Theorem · combinatorics

SimpleGraph.maxDegree_lt_card_verts

∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [Nonempty V],
  G.maxDegree < Fintype.card V

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.

Defined in

Mathlib.Combinatorics.SimpleGraph.Finite

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRelNonempty