Commit 2024-09-30 02:32 9a1a45ad
View on Github →feat (Topology/Instances/EReal): EReal.toReal
tends to top at top (#17100)
- Add
nhdsWithin_top
andnhdsWithin_bot
: the punctured neighbourhoods of top and bot inEReal
are the map ofatTop
andatBot
. - Add
tendsto_toReal_atTop
andtendsto_toReal_atBot
.