Commit 2022-02-10 08:34 e60ca6b4

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.