Add some missing map and set lemmas

I've needed these lemmas in several projects now. Most of these lemmas are straightforward adaptations of already existing lemmas on sets, and for these @robbertkrebbers said merging was "a complete no-brainer"

The lemma empty_difference (on sets and maps) is new, but it is very straightforward and canonical so I hope this can just be merged along.