feat(data/real/ennreal): use notation for ennreal (#6044)
The notation for `ennreal` is `ℝ≥0∞` and it is localized to `ennreal` (though I guess it doesn't have to be?).
Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20ennreal
