feat: introduce iterator combinators filterMap, filter and map

[datokrat]

This PR provides the iterator combinator filterMap in a pure and monadic version and specializations map and filter. This new combinator allows to apply a function to the emitted values of a stream while filtering out certain elements.

map should have an optimized IteratorCollect implementation but it turns out that this is not possible without a major refactor of IteratorCollect: toArrayMapped requires a proof that the iterator is finite. If it.mapM f is Finite but it is not, then such a proof does not exist. IteratorCollect needs to take a proof that the loop will terminate for the given monadic function f instead. This will not be done in this PR.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a12f89aefa10812fda01275d87bfc18d97914899 --onto 72141b05fd9a3328c1e5d99211dc4da4495cbd42. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-30 13:48:00)