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 and nhdsWithin_bot: the punctured neighbourhoods of top and bot in EReal are the map of atTop and atBot.
  • Add tendsto_toReal_atTop and tendsto_toReal_atBot.

Estimated changes

added theorem EReal.nhdsWithin_bot
added theorem EReal.nhdsWithin_top