degree_compl — Mathlib

English

In the complement graph Gᶜ, the degree of v equals |V| - 1 minus the degree in G.

Русский

В комплементарном графе Gᶜ степень вершины v равна |V| - 1 минус степень в графе G.

LaTeX

$$$ G^{\mathrm{c}}.degree v = |V| - 1 - G.degree v $$$

Lean4

theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] : Gᶜ.degree v = Fintype.card V - 1 - G.degree v := by
  classical
  rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
  simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]

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