mathlib

68d7d001 - chore(analysis/special_functions/pow): versions of tendsto/continuous_at lemmas for (e)nnreal (#8113)

chore(analysis/special_functions/pow): versions of tendsto/continuous_at lemmas for (e)nnreal (#8113) We have the full suite of lemmas about `tendsto` and `continuous` for real powers of `real`, but apparently not for `nnreal` or `ennreal`. I have provided a few, rather painfully -- if there is a better way, golfing is welcome! Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>