Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.of_real_add_of_real

Modification history

2018-01-11 16:21

analysis/ennreal.lean

fix(analysis/ennreal): fix long-running proofs

Deleted ennreal.of_real_add_of_real View on Github →

2017-08-29 19:20

topology/ennreal.lean

feat(topology/ennreal): add extended non-negative real numbers

Added ennreal.of_real_add_of_real View on Github →