Theorems · Theorem · combinatorics

SimpleGraph.neighborFinset_eq_filter

∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] {v : V} [inst_1 : DecidableRel G.Adj],
  G.neighborFinset v = {w | G.Adj v w}

Defined in

Mathlib.Combinatorics.SimpleGraph.Finite

Cited by

6 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRel