Theorem EReal.nhdsWithin_top

Modification history

2024-09-30 02:32

Mathlib/Topology/Instances/EReal.lean

feat (Topology/Instances/EReal): `EReal.toReal` tends to top at top (#17100) …

Added EReal.nhdsWithin_top View on Github →