Commit 2024-06-25 17:24 92882dd7

View on Github →

feat(Topology/NNReal): add Real.map_toNNReal_atTop (#13983) ... and Real.comap_toNNReal_atTop

Estimated changes

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.tendsto_ofReal_nhds_top

Modified Mathlib/Topology/Instances/NNReal.lean

added theorem Real.comap_toNNReal_atTop

added theorem Real.map_toNNReal_atTop

added theorem Real.tendsto_toNNReal_atTop

added theorem Real.tendsto_toNNReal_atTop_iff

modified theorem tendsto_real_toNNReal_atTop