Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-30 18:33 4ef0ea8a

View on Github →

feat(topology/ennreal): add subtraction

Estimated changes

Modified order/complete_lattice.lean

Modified topology/ennreal.lean

added theorem Sup_eq_top

added theorem ennreal.Inf_add

added theorem ennreal.Sup_add

added theorem ennreal.add_sub_cancel_of_le

added theorem ennreal.le_add_left

added theorem ennreal.le_add_right

added theorem ennreal.le_sub_iff_add_le

added theorem ennreal.lt_iff_exists_of_real

added theorem ennreal.lt_of_add_lt_add_left

added theorem ennreal.not_infty_lt

added theorem ennreal.of_real_lt_infty

modified theorem ennreal.of_real_lt_of_real_iff

added theorem ennreal.sub_add_cancel_of_le

added theorem ennreal.sub_add_self_eq_max

added theorem ennreal.sub_eq_zero_of_le

added theorem ennreal.sub_infty

added theorem ennreal.sub_le_sub

added theorem ennreal.sub_zero

added theorem ennreal.zero_sub

added theorem lt_Sup_iff