Commit 2025-06-11 16:59 0a5ab60c

View on Github →

chore: use Filter.map instead of <$> (#25694) <$> on Filter is not polymorphic and not simp-normal form.

Estimated changes

Modified Mathlib/Order/Filter/Map.lean

modified theorem Filter.map_swap_eq_comap_swap

Modified Mathlib/Topology/UniformSpace/Defs.lean

modified theorem uniformity_eq_symm

modified theorem uniformity_le_symm