Stream: math-comp analysis

Topic: instanciate near


view this post on Zulip Laurent Théry (Jul 08 2021 at 13:00):

I have an assumption that is {near x, continuous f} is there a direct way to get {for x, continuous f}

view this post on Zulip Cyril Cohen (Jul 08 2021 at 13:12):

nbhs_singleton ?

view this post on Zulip Cyril Cohen (Jul 08 2021 at 13:14):

Cyril Cohen said:

nbhs_singleton ?

I think the name is bad not intuitive enough (it's inherited from coquelicot's locally_singleton) and that we should change the name ASAP


Last updated: Apr 20 2024 at 00:02 UTC