compl — Mathlib

English

If G is d-regular, then its complement (G^c) is regular of degree |V| - 1 - d.

Русский

Если G — d-регулярный, то его дополнение (G^c) регулярно степени |V| - 1 - d.

LaTeX

$$G.IsRegularOfDegree k → (Gᶜ).IsRegularOfDegree (Fintype.card V - 1 - k)$$

Lean4

theorem compl [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} (h : G.IsRegularOfDegree k) :
    Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k) := by
  intro v
  rw [degree_compl, h v]

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