Commit 2024-09-30 02:03 856178f8

chore(Topology): move a folder (#17256) Move Topology/ContinuousFunction to Topology/ContinuousMap so that it agrees with the type name. This PR was generated by the following commands:

git mv Mathlib/Topology/ContinuousFunction Mathlib/Topology/ContinuousMap
git grep -l 'Topology.ContinuousF' | xargs sed -e 's/Topology.ContinuousFunction/Topology.ContinuousMap/' -i
lake exe mk_all --git