Add lemmas `map_intersection_filter` and `map_difference_filter`.

See also the discussion in iris!697 (diffs, comment 69805)

added 1 commit

• 1c34186e - Add lemmas `map_intersection_filter` and `map_difference_filter`.

Compare with previous version

changed title from Add lemmas intersection_filter and difference_filter. to Add lemmas {+map_+}intersection_filter and {+map_+}difference_filter.

Note that there's:

Lemma map_filter_union {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) :
  m1 ##ₘ m2 →
  filter P (m1 ∪ m2) = filter P m1 ∪ filter P m2.

We could have similar lemmas (map_filter_intersection and map_filter_difference) for ∩ and ∖. The naming in this MR (where filter appears at a different position), still allows for that.

That said, suggestions for better names for the lemmas in this MR are welcome too.

added 3 commits

• 1c34186e...3722f090 - 2 commits from branch master
• 14f8c75e - Add lemmas `map_intersection_filter` and `map_difference_filter`.

Compare with previous version

LGTM.

merged

mentioned in commit 5b54d2cb