Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.inv_limsup

Modification history

2022-02-10 08:34

src/topology/instances/ennreal.lean

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

Added ennreal.inv_limsup View on Github →