Mathlib v3 is deprecated. Go to Mathlib v4

Inductive ennreal

Modification history

2018-08-21 21:22

data/real/ennreal.lean

refactor(analysis/ennreal): use canonically_ordered_comm_semiring (with_top α)

Deleted ennreal View on Github →

2018-07-21 02:09

analysis/ennreal.lean

refactor(analysis/ennreal): split and move to data.real

Modified ennreal View on Github →

2017-08-29 19:20

topology/ennreal.lean

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

Added ennreal View on Github →