More lemmas for `filter` w.r.t. maps

• filter P m ##ₘ filter (λ v, ¬ P v) m
• filter P m ∪ filter (λ v, ¬ P v) m = m
• (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) → dom D (filter P m) ≡ X

For the last one, I have repurposed the name dom_map_filter, which was previously used for dom D (filter P m) ⊆ dom D m. I have renamed the old lemma into dom_map_filter_subseteq. This follows current naming conventions.

This MR received partial contributions from @dfrumin.

lgtm! thanks. those are enough for my lemma

merged

mentioned in commit f53dfb6d

Merged, thanks!