Theorems · Theorem · combinatorics

SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card

∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {s : V}
  (h : G.IsTuranMaximal r) [inst_2 : DecidableEq V], G.degree s = Fintype.card V - (h.finpartition.part s).card

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRelDecidableEq