constructor
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v ↔ a✝ ∈ M.A \ MultiPart.P M i
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v → a✝ ∈ M.A \ MultiPart.P M i

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → a✝ ∈ neighborFinset (mp M) v