no goals
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
f : ι → Subgraph G
v : V
⊢ neighborSet (⨅ (i : ι), f i) v = (⋂ (i : ι), neighborSet (f i) v) ∩ SimpleGraph.neighborSet G v
simp [iInf]