Theorem EReal.tendsto_toReal_atTop

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.tendsto_toReal_atTop View on Github →