Mathlib v3 is deprecated. Go to Mathlib v4

Def ennreal.inv_order_iso

Modification history

2022-02-11 01:36
src/data/real/ennreal.lean
chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for `inv` (#11959) …
Deleted ennreal.inv_order_isoView on Github →
2022-02-10 08:34
src/data/real/ennreal.lean
feat(data/real/ennreal): `inv` is an `order_iso` to the order dual and lemmas for `supr, infi` (#11869) …
Added ennreal.inv_order_isoView on Github →