Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-21 02:09 fb952fe4

View on Github →

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

Estimated changes

Modified analysis/ennreal.lean

deleted theorem ennreal.add_infty

deleted theorem ennreal.add_left_inj

deleted theorem ennreal.add_right_inj

deleted theorem ennreal.add_sub_cancel_of_le

deleted theorem ennreal.add_sub_self'

deleted theorem ennreal.add_sub_self

deleted theorem ennreal.forall_ennreal

deleted theorem ennreal.infty_add

deleted theorem ennreal.infty_le_iff

deleted theorem ennreal.infty_mem_upper_bounds

deleted theorem ennreal.infty_mul

deleted theorem ennreal.infty_mul_of_real

deleted theorem ennreal.infty_ne_of_real

deleted theorem ennreal.infty_ne_zero

deleted theorem ennreal.infty_sub_of_real

deleted theorem ennreal.inv_infty

deleted theorem ennreal.inv_inv

deleted theorem ennreal.inv_of_real

deleted theorem ennreal.inv_zero

deleted theorem ennreal.is_lub_of_real

deleted theorem ennreal.le_add_left

deleted theorem ennreal.le_add_right

deleted theorem ennreal.le_def

deleted theorem ennreal.le_infty

deleted theorem ennreal.le_of_forall_epsilon_le

deleted theorem ennreal.le_of_real_iff

deleted theorem ennreal.le_zero_iff_eq

deleted theorem ennreal.lt_add_right

deleted theorem ennreal.lt_iff_exists_of_real

deleted theorem ennreal.mul_infty

deleted theorem ennreal.mul_le_mul

deleted theorem ennreal.not_infty_lt

deleted theorem ennreal.not_lt_zero

deleted def ennreal.of_ennreal

deleted theorem ennreal.of_ennreal_of_real

deleted theorem ennreal.of_nonneg_real_eq_of_real

deleted def ennreal.of_real

deleted theorem ennreal.of_real_add

deleted theorem ennreal.of_real_add_le

deleted theorem ennreal.of_real_eq_of_real_of

deleted theorem ennreal.of_real_eq_one_iff

deleted theorem ennreal.of_real_eq_zero_iff

deleted theorem ennreal.of_real_le_of_real

deleted theorem ennreal.of_real_le_of_real_iff

deleted theorem ennreal.of_real_lt_infty

deleted theorem ennreal.of_real_lt_of_real_iff

deleted theorem ennreal.of_real_lt_of_real_iff_cases

deleted theorem ennreal.of_real_mem_upper_bounds

deleted theorem ennreal.of_real_mul_infty

deleted theorem ennreal.of_real_mul_of_real

deleted theorem ennreal.of_real_ne_infty

deleted theorem ennreal.of_real_ne_of_real_of

deleted theorem ennreal.of_real_of_ennreal

deleted theorem ennreal.of_real_of_nonpos

deleted theorem ennreal.of_real_of_not_nonneg

deleted theorem ennreal.of_real_one

deleted theorem ennreal.of_real_sub_of_real

deleted theorem ennreal.of_real_zero

deleted theorem ennreal.one_eq_of_real_iff

deleted theorem ennreal.one_le_of_real_iff

deleted theorem ennreal.sub_add_cancel_of_le

deleted theorem ennreal.sub_add_self_eq_max

deleted theorem ennreal.sub_eq_zero_of_le

deleted theorem ennreal.sub_infty

deleted theorem ennreal.sub_le_self

deleted theorem ennreal.sub_le_sub

deleted theorem ennreal.sub_sub_cancel

deleted theorem ennreal.sub_zero

deleted theorem ennreal.sum_of_real

deleted theorem ennreal.zero_eq_of_real_iff

deleted theorem ennreal.zero_le_of_ennreal

deleted theorem ennreal.zero_lt_of_real_iff

deleted theorem ennreal.zero_ne_infty

deleted theorem ennreal.zero_sub

deleted inductive ennreal

Modified data/real/basic.lean

added theorem real.Sup_is_lub

Created data/real/ennreal.lean

added theorem ennreal.add_infty

added theorem ennreal.add_left_inj

added theorem ennreal.add_right_inj

added theorem ennreal.add_sub_cancel_of_le

added theorem ennreal.add_sub_self'

added theorem ennreal.add_sub_self

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.infty_sub_of_real

added theorem ennreal.inv_infty

added theorem ennreal.inv_inv

added theorem ennreal.inv_of_real

added theorem ennreal.inv_zero

added theorem ennreal.is_lub_of_real

added theorem ennreal.le_add_left

added theorem ennreal.le_add_right

added theorem ennreal.le_def

added theorem ennreal.le_infty

added theorem ennreal.le_of_forall_epsilon_le

added theorem ennreal.le_of_real_iff

added theorem ennreal.le_zero_iff_eq

added theorem ennreal.lt_add_right

added theorem ennreal.lt_iff_exists_of_real

added theorem ennreal.mul_infty

added theorem ennreal.mul_le_mul

added theorem ennreal.not_infty_lt

added theorem ennreal.not_lt_zero

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

added theorem ennreal.of_real_add_le

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

added theorem ennreal.of_real_le_of_real_iff

added theorem ennreal.of_real_lt_infty

added theorem ennreal.of_real_lt_of_real_iff

added theorem ennreal.of_real_lt_of_real_iff_cases

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_of_nonpos

added theorem ennreal.of_real_of_not_nonneg

added theorem ennreal.of_real_one

added theorem ennreal.of_real_sub_of_real

added theorem ennreal.of_real_zero

added theorem ennreal.one_eq_of_real_iff

added theorem ennreal.one_le_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_self

added theorem ennreal.sub_le_sub

added theorem ennreal.sub_sub_cancel

added theorem ennreal.sub_zero

added theorem ennreal.sum_of_real

added theorem ennreal.zero_eq_of_real_iff

added theorem ennreal.zero_le_of_ennreal

added theorem ennreal.zero_lt_of_real_iff

added theorem ennreal.zero_ne_infty

added theorem ennreal.zero_sub

added inductive ennreal

Modified data/set/lattice.lean

added def set.kern_image

Modified order/bounds.lean

Modified order/galois_connection.lean

deleted def set.kern_image