Theorems · Theorem · combinatorics

SimpleGraph.compl_neighborFinset_sdiff_inter_eq

∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V] {v w : V},
  (G.neighborFinset v)ᶜ \ {v} ∩ ((G.neighborFinset w)ᶜ \ {w}) =
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v})

Defined in: Mathlib.Combinatorics.SimpleGraph.StronglyRegular
Cited by: 2 results in Mathlib
Foundations: Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableRel DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
Fintypestatement and proof · cited by 7,736
SimpleGraphstatement and proof · cited by 3,072
Compl.complstatement · cited by 2,925
SimpleGraph.Adjstatement and proof · cited by 1,346
SimpleGraph.neighborSetstatement · cited by 257
SimpleGraph.neighborFinsetstatement · cited by 72

Cited by2

Results whose statement or proof uses this declaration.

SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_complproof · cited by 1
SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_complproof · cited by 1