Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 21:33 b9e559b7

View on Github →

feat(data/real/ennreal): use notation for ennreal (#6044) The notation for ennreal is ℝ≥0∞ and it is localized to ennreal (though I guess it doesn't have to be?). Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20ennreal

Estimated changes

modified theorem ennreal.lintegral_Lp_add_le
modified theorem ennreal.rpow_add_rpow_le
modified theorem ennreal.young_inequality
modified theorem edist_eq_coe_nnnorm
modified theorem edist_eq_coe_nnnorm_sub
modified theorem mem_emetric_ball_0_iff
modified theorem of_real_norm_eq_coe_nnnorm
modified theorem real.ennnorm_eq_of_real
modified theorem ennreal.div_rpow_of_nonneg
modified theorem ennreal.inv_rpow_of_pos
modified theorem ennreal.le_rpow_one_div_iff
modified theorem ennreal.lt_rpow_one_div_iff
modified theorem ennreal.measurable_rpow
modified theorem ennreal.mul_rpow_of_ne_top
modified theorem ennreal.mul_rpow_of_ne_zero
modified theorem ennreal.mul_rpow_of_nonneg
modified theorem ennreal.one_le_rpow
modified theorem ennreal.one_lt_rpow
modified theorem ennreal.one_rpow
modified theorem ennreal.rpow_add
modified theorem ennreal.rpow_eq_pow
modified theorem ennreal.rpow_eq_top_iff
modified theorem ennreal.rpow_eq_zero_iff
modified theorem ennreal.rpow_le_one
modified theorem ennreal.rpow_le_rpow
modified theorem ennreal.rpow_le_rpow_iff
modified theorem ennreal.rpow_lt_one
modified theorem ennreal.rpow_lt_rpow
modified theorem ennreal.rpow_lt_rpow_iff
modified theorem ennreal.rpow_mul
modified theorem ennreal.rpow_nat_cast
modified theorem ennreal.rpow_neg
modified theorem ennreal.rpow_neg_one
modified theorem ennreal.rpow_one
modified theorem ennreal.rpow_pos
modified theorem ennreal.rpow_pos_of_nonneg
modified theorem ennreal.rpow_zero
modified theorem ennreal.to_nnreal_rpow
modified theorem ennreal.to_real_rpow
modified theorem ennreal.top_rpow_def
modified theorem ennreal.top_rpow_of_neg
modified theorem ennreal.top_rpow_of_pos
modified theorem ennreal.zero_rpow_def
modified theorem ennreal.zero_rpow_of_neg
modified theorem ennreal.zero_rpow_of_pos
modified theorem measurable.ennreal_rpow
modified theorem ennreal.tsum_geometric
modified theorem ennreal.Inf_add
modified theorem ennreal.add_halves
modified theorem ennreal.add_infi
modified theorem ennreal.add_sub_self
modified theorem ennreal.bot_eq_zero
modified theorem ennreal.cinfi_ne_top
modified theorem ennreal.coe_Inf
modified theorem ennreal.coe_Sup
modified theorem ennreal.coe_add
modified theorem ennreal.coe_bit0
modified theorem ennreal.coe_bit1
modified theorem ennreal.coe_div
modified theorem ennreal.coe_eq_coe
modified theorem ennreal.coe_eq_one
modified theorem ennreal.coe_eq_zero
modified theorem ennreal.coe_inv
modified theorem ennreal.coe_inv_le
modified theorem ennreal.coe_inv_two
modified theorem ennreal.coe_le_coe
modified theorem ennreal.coe_le_one_iff
modified theorem ennreal.coe_lt_coe
modified theorem ennreal.coe_lt_coe_nat
modified theorem ennreal.coe_lt_one_iff
modified theorem ennreal.coe_max
modified theorem ennreal.coe_min
modified theorem ennreal.coe_mono
modified theorem ennreal.coe_mul
modified theorem ennreal.coe_nat
modified theorem ennreal.coe_nat_le_coe_nat
modified theorem ennreal.coe_nat_lt_coe
modified theorem ennreal.coe_nat_lt_coe_nat
modified theorem ennreal.coe_nat_mono
modified theorem ennreal.coe_nat_ne_top
modified theorem ennreal.coe_ne_top
modified theorem ennreal.coe_nnreal_eq
modified theorem ennreal.coe_nonneg
modified theorem ennreal.coe_one
modified theorem ennreal.coe_pos
modified theorem ennreal.coe_pow
modified theorem ennreal.coe_sub
modified theorem ennreal.coe_to_nnreal
modified theorem ennreal.coe_to_real
modified theorem ennreal.coe_two
modified theorem ennreal.coe_zero
modified theorem ennreal.csupr_ne_top
modified theorem ennreal.div_add_div_same
modified theorem ennreal.div_lt_top
modified theorem ennreal.div_one
modified theorem ennreal.exists_inv_nat_lt
modified theorem ennreal.exists_ne_top
modified theorem ennreal.forall_ennreal
modified theorem ennreal.forall_ne_top
modified theorem ennreal.half_lt_self
modified theorem ennreal.half_pos
modified theorem ennreal.infi_ennreal
modified theorem ennreal.infi_mul
modified theorem ennreal.infi_ne_top
modified theorem ennreal.infi_sum
modified theorem ennreal.inv_bijective
modified theorem ennreal.inv_involutive
modified theorem ennreal.inv_lt_top
modified theorem ennreal.inv_one
modified theorem ennreal.inv_two_add_inv_two
modified theorem ennreal.inv_zero
modified theorem ennreal.mul_infi
modified theorem ennreal.mul_le_iff_le_inv
modified theorem ennreal.mul_lt_top_iff
modified theorem ennreal.nat_ne_top
modified theorem ennreal.none_eq_top
modified theorem ennreal.not_lt_top
modified def ennreal.of_nnreal_hom
modified theorem ennreal.of_real_one
modified theorem ennreal.of_real_to_real
modified theorem ennreal.of_real_to_real_le
modified theorem ennreal.one_eq_coe
modified theorem ennreal.one_half_lt_one
modified theorem ennreal.one_le_coe_iff
modified theorem ennreal.one_lt_coe_iff
modified theorem ennreal.one_lt_two
modified theorem ennreal.one_sub_inv_two
modified theorem ennreal.one_to_nnreal
modified theorem ennreal.one_to_real
modified theorem ennreal.prod_lt_top
modified theorem ennreal.some_eq_coe
modified theorem ennreal.sub_le_self
modified theorem ennreal.sub_right_inj
modified theorem ennreal.sum_eq_top_iff
modified theorem ennreal.sum_lt_top
modified theorem ennreal.sum_lt_top_iff
modified theorem ennreal.supr_coe_nat
modified theorem ennreal.supr_ennreal
modified theorem ennreal.supr_ne_top
modified theorem ennreal.to_nnreal_add
modified theorem ennreal.to_nnreal_coe
modified def ennreal.to_nnreal_hom
modified theorem ennreal.to_nnreal_mul
modified theorem ennreal.to_nnreal_mul_top
modified theorem ennreal.to_nnreal_pow
modified theorem ennreal.to_nnreal_prod
modified theorem ennreal.to_nnreal_sum
modified theorem ennreal.to_nnreal_top_mul
modified theorem ennreal.to_real_eq_zero_iff
modified def ennreal.to_real_hom
modified theorem ennreal.to_real_mul_top
modified theorem ennreal.to_real_nonneg
modified theorem ennreal.to_real_of_real_mul
modified theorem ennreal.to_real_pow
modified theorem ennreal.to_real_prod
modified theorem ennreal.to_real_sum
modified theorem ennreal.to_real_top_mul
modified theorem ennreal.top_ne_coe
modified theorem ennreal.two_ne_top
modified theorem ennreal.two_ne_zero
modified theorem ennreal.zero_eq_coe
modified theorem ennreal.zero_lt_coe_iff
modified theorem ennreal.zero_lt_two
modified theorem ennreal.zero_to_nnreal
modified theorem ennreal.zero_to_real
modified theorem ae_measurable.ennreal_mul
modified theorem ae_measurable.to_real
modified theorem ennreal.measurable_coe
modified theorem ennreal.measurable_div
modified theorem ennreal.measurable_inv
modified theorem ennreal.measurable_mul
modified theorem ennreal.measurable_sub
modified theorem measurable.ennreal_div
modified theorem measurable.ennreal_inv
modified theorem measurable.ennreal_mul
modified theorem measurable.ennreal_sub
modified theorem measurable.ennreal_tsum
modified theorem measurable.to_nnreal
modified theorem measurable.to_real
modified theorem measurable_ennnorm
modified theorem ennreal.ae_le_ess_sup
modified theorem ennreal.ess_sup_add_le
modified theorem ennreal.ess_sup_const_mul
modified theorem ennreal.ess_sup_eq_zero_iff
modified theorem measure_theory.ae_lt_top
modified theorem measure_theory.Lp.antimono
modified def measure_theory.snorm'
modified def measure_theory.snorm
modified theorem ae_measurable.smul_measure
modified def measure_theory.extend
modified theorem ennreal.limsup_add_le
modified theorem ennreal.limsup_const_mul
modified theorem ennreal.limsup_eq_zero_iff
modified theorem continuous_of_le_add_edist
modified theorem edist_ne_top_of_mem_ball
modified theorem emetric.is_closed_ball
modified theorem ennreal.Sup_add
modified theorem ennreal.add_supr
modified theorem ennreal.bsupr_add
modified theorem ennreal.coe_range_mem_nhds
modified theorem ennreal.continuous_coe
modified theorem ennreal.embedding_coe
modified theorem ennreal.finset_sum_supr_nat
modified theorem ennreal.infi_mul_left
modified theorem ennreal.infi_mul_right
modified theorem ennreal.is_open_ne_top
modified theorem ennreal.mul_Sup
modified theorem ennreal.mul_supr
modified theorem ennreal.nhds_coe
modified theorem ennreal.nhds_coe_coe
modified theorem ennreal.nhds_zero
modified theorem ennreal.sub_supr
modified theorem ennreal.supr_add
modified theorem ennreal.supr_add_supr
modified theorem ennreal.supr_eq_zero
modified theorem ennreal.supr_mul
modified theorem ennreal.tendsto_nhds_top
modified theorem ennreal.tendsto_sum_nat_add
modified theorem ennreal.tendsto_to_nnreal
modified theorem ennreal.tendsto_to_real
modified theorem ennreal.tsum_sub
modified theorem ennreal.tsum_supr_eq
modified theorem nhds_eq_nhds_emetric_ball
modified theorem edist_mem_uniformity
modified def emetric.ball
modified theorem emetric.ball_mem_nhds
modified theorem emetric.ball_prod_same
modified def emetric.closed_ball
modified theorem emetric.diam_ball
modified theorem emetric.diam_closed_ball
modified theorem emetric.nhds_basis_eball
modified theorem uniformity_basis_edist'
modified theorem uniformity_basis_edist_le'
modified def emetric.inf_edist
modified theorem ennreal.half_lt_self_bis