mathlib

e60ca6b4 - feat(data/real/ennreal): `inv` is an `order_iso` to the order dual and lemmas for `supr, infi` (#11869)

feat(data/real/ennreal): `inv` is an `order_iso` to the order dual and lemmas for `supr, infi` (#11869) Establishes that `inv` is an order isomorphism to the order dual. We then provide some convenience lemmas which guarantee that `inv` switches `supr` and `infi` and hence also switches `limsup` and `liminf`.