constructor
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a✝ ∈ nbhdRes (mp M) v M.A
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A → a✝ ∈ nbhdRes (mp M) v M.A

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp M) v M.A → a✝ ∈ nbhdRes (mp (minsert M h)) v M.A