Mathlib Changelog
v3
Changelog
About
Github
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