Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-16 07:31 78940f46

View on Github →

chore(*): use notation ℝ≥0 (#5391)

Estimated changes

modified theorem continuous_nnnorm
modified theorem lipschitz_with.add
modified theorem lipschitz_with.neg
modified theorem lipschitz_with.sub
modified theorem summable_of_nnnorm_bounded
modified theorem measurable.nnreal_rpow
modified theorem nnreal.measurable_rpow
modified theorem nnreal.has_sum_geometric
modified theorem nnreal.summable_geometric
modified theorem tsum_geometric_nnreal
modified theorem nnreal.add_sub_cancel'
modified theorem nnreal.add_sub_cancel
modified theorem nnreal.bdd_above_coe
modified theorem nnreal.bdd_below_coe
modified theorem nnreal.bot_eq_zero
modified theorem nnreal.coe_Inf
modified theorem nnreal.coe_Sup
modified theorem nnreal.coe_max
modified theorem nnreal.coe_min
modified theorem nnreal.coe_nonneg
modified theorem nnreal.div_def
modified theorem nnreal.inv_eq_zero
modified theorem nnreal.inv_pos
modified theorem nnreal.inv_zero
modified theorem nnreal.lt_sub_iff_add_lt
modified theorem nnreal.mul_eq_mul_left
modified theorem nnreal.mul_ne_zero'
modified theorem nnreal.sub_add_cancel_of_le
modified theorem nnreal.sub_eq_iff_eq_add
modified theorem nnreal.sub_le_iff_le_add
modified theorem nnreal.sub_lt_iff_lt_add
modified theorem nnreal.val_eq_coe
modified theorem nnreal.zero_le_coe
modified theorem ennreal.coe_range_mem_nhds
modified theorem ennreal.continuous_coe
modified theorem ennreal.continuous_coe_iff
modified theorem ennreal.embedding_coe
modified theorem ennreal.nhds_coe
modified theorem ennreal.nhds_coe_coe
modified theorem ennreal.tendsto_coe
modified theorem dist_le_coe
modified theorem dist_lt_coe
modified theorem edist_le_coe
modified theorem edist_lt_coe
modified theorem metric.emetric_ball_nnreal
modified def nndist
modified theorem nnreal.dist_eq
modified theorem nnreal.nndist_eq