Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ennreal.not_infty_lt

Modification history

2018-08-21 22:05

data/real/ennreal.lean

refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal

Deleted ennreal.not_infty_lt View on Github →

2018-07-21 02:09

analysis/ennreal.lean

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

Modified ennreal.not_infty_lt View on Github →

2017-08-30 18:33

topology/ennreal.lean

feat(topology/ennreal): add subtraction

Added ennreal.not_infty_lt View on Github →