Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-29 19:20 51042cde

View on Github →

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

Estimated changes

Modified algebra/big_operators.lean

Created topology/ennreal.lean

added theorem ennreal.add_infty

added theorem ennreal.add_le_add

added theorem ennreal.forall_ennreal

added theorem ennreal.infty_add

added theorem ennreal.infty_le_iff

added theorem ennreal.infty_mem_upper_bounds

added theorem ennreal.infty_mul

added theorem ennreal.infty_mul_of_real

added theorem ennreal.infty_ne_of_real

added theorem ennreal.infty_ne_zero

added theorem ennreal.is_lub_of_real

added theorem ennreal.le_infty

added theorem ennreal.le_of_real_iff

added theorem ennreal.le_zero_iff_eq

added theorem ennreal.mul_infty

added theorem ennreal.mul_le_mul

added def ennreal.of_ennreal

added theorem ennreal.of_ennreal_of_real

added theorem ennreal.of_nonneg_real_eq_of_real

added def ennreal.of_real

added theorem ennreal.of_real_add_of_real

added theorem ennreal.of_real_eq_of_real_of

added theorem ennreal.of_real_eq_one_iff

added theorem ennreal.of_real_eq_zero_iff

added theorem ennreal.of_real_le_of_real_iff

added theorem ennreal.of_real_lt_of_real_iff

added theorem ennreal.of_real_mem_upper_bounds

added theorem ennreal.of_real_mul_infty

added theorem ennreal.of_real_mul_of_real

added theorem ennreal.of_real_ne_infty

added theorem ennreal.of_real_ne_of_real_of

added theorem ennreal.of_real_of_ennreal

added theorem ennreal.of_real_one

added theorem ennreal.of_real_zero

added theorem ennreal.one_eq_of_real_iff

added theorem ennreal.zero_eq_of_real_iff

added theorem ennreal.zero_le_of_ennreal

added theorem ennreal.zero_ne_infty

added inductive ennreal

added theorem zero_le_mul

Modified topology/real.lean

modified theorem exists_supremum_real