generalize `cvg_nbhsP` in `realfun.v` to any metric space

Open affeldt-aist opened this issue 1 year ago • 1 comments

For the record, comment from PR #1396 by @zstone1 : "It would be nice to have this for any metric space (or indeed any first-countable space). But it's fine to have the specialized version for now if it's useful. We can always go back and generalize later"

Dec 17 '24 15:12 affeldt-aist

depends on PR #1589

Jun 28 '25 08:06 affeldt-aist