Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 16:39 e7579363

View on Github →

chore(data/real/ennreal, measure_theory/): use ≠ ∞ and ≠ 0 in assumptions (#9219)

Estimated changes

modified theorem with_top.sum_lt_top
modified theorem with_top.mul_lt_top
modified theorem ennreal.add_left_inj
modified theorem ennreal.add_right_inj
modified theorem ennreal.add_sub_self'
modified theorem ennreal.add_sub_self
added theorem ennreal.coe_ne_zero
modified theorem ennreal.div_lt_top
added theorem ennreal.div_zero
modified theorem ennreal.half_pos
added theorem ennreal.le_to_real_sub
modified theorem ennreal.lt_add_right
modified theorem ennreal.mem_Iio_self_add
modified theorem ennreal.mul_lt_top
modified theorem ennreal.mul_pos
added theorem ennreal.mul_pos_iff
modified theorem ennreal.pow_eq_top
added theorem ennreal.pow_eq_top_iff
modified theorem ennreal.prod_lt_top
modified theorem ennreal.sub_right_inj
modified theorem ennreal.sub_sub_cancel
modified theorem ennreal.sum_lt_top
modified theorem ennreal.to_nnreal_add
modified theorem ennreal.to_nnreal_sum
modified theorem ennreal.to_real_eq_to_real
modified theorem ennreal.to_real_sum
deleted theorem ennreal.zero_lt_coe_iff
modified theorem measure_theory.ae_lt_top'
modified theorem measure_theory.ae_lt_top
modified theorem ennreal.Icc_mem_nhds
modified theorem ennreal.nhds_of_ne_top
modified theorem ennreal.tsum_sub
modified theorem edist_ne_top
modified theorem lipschitz_with.edist_lt_top