minDegree_lt_card — Mathlib

English

In a nonempty graph, the minimal degree is less than the number of vertices.

Русский

В непустом графе минимальная степень меньше числа вершин.

LaTeX

$$G.minDegree < Fintype.card V$$

Lean4

/-- In a nonempty graph, the minimal degree is less than the number of vertices. -/
theorem minDegree_lt_card [DecidableRel G.Adj] [Nonempty V] : G.minDegree < Fintype.card V :=
  by
  obtain ⟨v, hδ⟩ := G.exists_minimal_degree_vertex
  rw [hδ, ← card_neighborFinset_eq_degree, ← card_univ]
  have h : v ∉ G.neighborFinset v := (G.mem_neighborFinset v v).not.mpr (G.loopless v)
  contrapose! h
  rw [eq_of_subset_of_card_le (subset_univ _) h]
  exact mem_univ v

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