mathlib3

6490ee3a - feat(topology/instances/ennreal): Add lemmas about continuity of ennreal subtraction. (#13448)

feat(topology/instances/ennreal): Add lemmas about continuity of ennreal subtraction. (#13448) `ennreal` does not have continuous `sub`. This PR adds `ennreal.continuous_on_sub` and related lemmas, which give the continuity of the subtraction in more restricted/specialized setups.