Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.bsupr_add'

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.bsupr_add'View on Github →