Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.add_bsupr

Modification history

2022-05-23 01:49

src/topology/instances/ennreal.lean

feat(topology/instances/ennreal): golf, add lemmas about `supr_add_supr` (#14274) …

Added ennreal.add_bsupr View on Github →