Rename RBSet.map to RBSet.mapMonotonic?

Stream: batteries

[Chris Wong]

The current RBSet.map requires that the mapping function is monotonic.

This differs from the convention in OCaml and Haskell, where the default map doesn't require monotonicity.

Can we rename this to mapMonotonic, and introduce a non-monotonic map f := ofList ∘ List.map f ∘ toList ?

[Mario Carneiro]

Finset also has separate map and image functions, with the former requiring injectivity

[Chris Wong]

Filed a PR: https://github.com/leanprover/std4/pull/274