feat(topology/basic): a condition implying that a sequence of functions locally stabilizes (#15580)
feat(topology/basic): a condition implying that a sequence of functions locally stabilizes (#15580)

For sphere-eversion-project.



Co-authored-by: Patrick Massot <32f9b1fcd0a495248bb312c163462b2098efe57d@free.fr>

leanprover-community/mathlib,leanprover-community/mathlib