Mathlib Changelog
v3
Changelog
About
Github
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
src/analysis/ODE/gronwall.lean
Modified
src/analysis/analytic/basic.lean
modified
theorem
formal_multilinear_series.bound_of_lt_radius
modified
theorem
formal_multilinear_series.geometric_bound_of_lt_radius
modified
theorem
formal_multilinear_series.le_radius_of_bound
modified
theorem
has_fpower_series_on_ball.tendsto_uniformly_on'
modified
theorem
has_fpower_series_on_ball.tendsto_uniformly_on
modified
theorem
has_fpower_series_on_ball.uniform_geometric_approx
Modified
src/analysis/analytic/composition.lean
Modified
src/analysis/mean_inequalities.lean
Modified
src/analysis/normed_space/basic.lean
modified
theorem
antilipschitz_with.add_lipschitz_with
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
src/analysis/normed_space/operator_norm.lean
modified
theorem
continuous_linear_map.op_norm_le_of_lipschitz
modified
theorem
continuous_linear_map.uniform_embedding_of_bound
modified
theorem
linear_map.antilipschitz_of_bound
Modified
src/analysis/special_functions/pow.lean
modified
theorem
measurable.nnreal_rpow
modified
theorem
measurable.nnreal_rpow_const
modified
theorem
nnreal.measurable_rpow
modified
theorem
nnreal.measurable_rpow_const
Modified
src/analysis/specific_limits.lean
modified
theorem
nnreal.exists_pos_sum_of_encodable
modified
theorem
nnreal.has_sum_geometric
modified
theorem
nnreal.summable_geometric
modified
theorem
nnreal.tendsto_const_div_at_top_nhds_0_nat
modified
theorem
nnreal.tendsto_inverse_at_top_nhds_0_nat
modified
theorem
nnreal.tendsto_pow_at_top_nhds_0_of_lt_1
modified
theorem
tsum_geometric_nnreal
Modified
src/data/real/ennreal.lean
Modified
src/data/real/nnreal.lean
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.le_of_forall_epsilon_le
modified
theorem
nnreal.le_of_real_iff_coe_le
modified
theorem
nnreal.lt_iff_exists_rat_btwn
modified
theorem
nnreal.lt_of_real_iff_coe_lt
modified
theorem
nnreal.lt_sub_iff_add_lt
modified
theorem
nnreal.mul_eq_mul_left
modified
theorem
nnreal.mul_ne_zero'
modified
theorem
nnreal.of_real_le_iff_le_coe
modified
theorem
nnreal.of_real_lt_iff_lt_coe
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
src/measure_theory/bochner_integration.lean
modified
theorem
measure_theory.lintegral_coe_eq_integral
Modified
src/measure_theory/content.lean
modified
theorem
measure_theory.outer_measure.of_content_exists_compact
modified
theorem
measure_theory.outer_measure.of_content_exists_open
Modified
src/measure_theory/decomposition.lean
Modified
src/measure_theory/integration.lean
modified
theorem
measure_theory.lintegral_mono_nnreal
modified
theorem
measure_theory.simple_func.map_coe_ennreal_restrict
modified
theorem
measure_theory.simple_func.map_coe_nnreal_restrict
Modified
src/measure_theory/outer_measure.lean
Modified
src/topology/algebra/infinite_sum.lean
modified
theorem
cauchy_seq_of_edist_le_of_summable
Modified
src/topology/bounded_continuous_function.lean
modified
def
bounded_continuous_function.comp
modified
theorem
bounded_continuous_function.continuous_comp
modified
theorem
bounded_continuous_function.lipschitz_comp
modified
theorem
bounded_continuous_function.uniform_continuous_comp
Modified
src/topology/instances/ennreal.lean
modified
theorem
ennreal.coe_range_mem_nhds
modified
theorem
ennreal.continuous_coe
modified
theorem
ennreal.continuous_coe_iff
modified
theorem
ennreal.embedding_coe
modified
def
ennreal.lt_top_homeomorph_nnreal
modified
def
ennreal.ne_top_homeomorph_nnreal
modified
theorem
ennreal.nhds_coe
modified
theorem
ennreal.nhds_coe_coe
modified
theorem
ennreal.tendsto_coe
Modified
src/topology/metric_space/antilipschitz.lean
Modified
src/topology/metric_space/basic.lean
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
theorem
metric.emetric_closed_ball_nnreal
modified
def
nndist
modified
theorem
nnreal.dist_eq
modified
theorem
nnreal.nndist_eq
Modified
src/topology/metric_space/emetric_space.lean
Modified
src/topology/metric_space/gromov_hausdorff_realized.lean
Modified
src/topology/metric_space/hausdorff_distance.lean
Modified
src/topology/metric_space/lipschitz.lean
Modified
src/topology/metric_space/pi_Lp.lean