Commit 2025-10-30 16:30 b3dd7d50

feat(Topology): split Mathlib.Topology.ContinuousOn (#31090) Move basic API on relative neighbourhood filters from Mathlib.Topology.ContinuousOn into a new file Mathlib.Topology.NhdsWithin. The reason we list Jeremy Avigad and Sébastien Gouëzel as authors in the copyright notice of the new file instead of copying over the copyright notice from the old is that according to this git blame, they wrote most of the API on nhds_within in topology.basic before it got moved to topology.continuous_on in [mathlib3#1516](https://github.com/leanprover-community/mathlib3/pull/1516), the PR to which the current copyright notice in Topology.ContinuousOn dates back.