Theorems · Theorem · combinatorics

SimpleGraph.disjoint_sdiff_neighborFinset_image

∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  Disjoint (G.edgeFinset \ G.incidenceFinset t) (Finset.image (fun x => s(x, t)) (G.neighborFinset s))

Defined in

Mathlib.Combinatorics.SimpleGraph.Operations

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableRel