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](https://github.com/leanprover-community/mathlib3/blame/b3eb34d29588efff46a2c465e66f5ef67c036a47/src/topology/basic.lean), they wrote most of the API on `nhds_within` in `topology.basic` before it got moved to `topology.continuous_on` in [mathlib3#1516](leanprover-community/mathlib3#1516), the PR to which the current copyright notice in `Topology.ContinuousOn` dates back.

Author: peabrainiac

Mathlib.lean

@@ -6915,6 +6915,7 @@ import Mathlib.Topology.NatEmbedding
 import Mathlib.Topology.Neighborhoods
 import Mathlib.Topology.NhdsKer
 import Mathlib.Topology.NhdsSet
+import Mathlib.Topology.NhdsWithin
 import Mathlib.Topology.NoetherianSpace
 import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.OpenPartialHomeomorph

Mathlib/Topology/Bases.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import Mathlib.Data.Set.Constructions
 import Mathlib.Order.Filter.AtTopBot.CountablyGenerated
 import Mathlib.Topology.Constructions
-import Mathlib.Topology.ContinuousOn
+import Mathlib.Topology.NhdsWithin
 
 /-!
 # Bases of topologies. Countability axioms.