# Make filter lemmas for maps and sets consistent + add cross split property for maps

We have the following lemmas for the combination of filter and union/disjoint for maps and sets:

```
Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P m ∪ filter (λ v, ¬ P v) m = m.
Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P m ##ₘ filter (λ v, ¬ P v) m.
Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
```

There are two things that are strange here:

- The naming scheme is inconsistent:
`union_filter`

vs`filter_union`

- The statements of the union+filter lemmas is inconsistent

This MR aims to make the set of lemmas for maps and sets consistent. Concretely:

- Sets: Add lemmas
`disjoint_filter`

,`disjoint_filter_complement`

, and`filter_union_complement`

. - Maps: Rename
`map_disjoint_filter`

→`map_disjoint_filter_complement`

and`map_union_filter`

→`map_filter_union_complement`

to be consistent with sets. - Maps: Add lemmas
`map_disjoint_filter`

and`map_filter_union`

analogous to sets. - Maps: Use filter lemmas to prove cross split property.

Edited by Robbert Krebbers