Theorem: SimpleGraph.mem_res_nbhd_iff (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
⊢ w ∈ nbhdRes G v A ↔ w ∈ A ∧ w ∈ neighborFinset G v
Tactic:
rw [nbhdRes, mem_inter]
State after:
no goals