Commit 2025-05-03 04:57 f4e4c914

View on Github →

feat(Topology/Inseparable): more mapping lemmas (#24526) Prove Specializes.map_of_continuousWithinAt, Specializes.map_of_continuousOn, and Inseparable.map_of_continuousWithinAt, Inseparable.map_of_continuousOn.

Estimated changes

Modified Mathlib/Topology/Inseparable.lean

added theorem Inseparable.map_of_continuousOn

added theorem Inseparable.map_of_continuousWithinAt

modified theorem Specializes.map_of_continuousAt

added theorem Specializes.map_of_continuousOn

added theorem Specializes.map_of_continuousWithinAt