complete_graph_degree — Mathlib

English

In the complete graph on V, every vertex has degree |V| - 1.

Русский

В полном графе на множестве V каждая вершина имеет степень |V| - 1.

LaTeX

$$(\deg_{\mathrm{completeGraph}(V)}(v)) = |V| - 1$$

Lean4

@[simp]
theorem complete_graph_degree [DecidableEq V] (v : V) : (completeGraph V).degree v = Fintype.card V - 1 :=
  by
  simp_rw [degree, neighborFinset_eq_filter, top_adj, filter_ne]
  rw [card_erase_of_mem (mem_univ v), card_univ]

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