feat(topology/basic): add explicit definition of continuous_at (#11296)
feat(topology/basic): add explicit definition of continuous_at (#11296)

This was convenient in a demo.





leanprover-community/mathlib,leanprover-community/mathlib