Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-31 20:17 0827f3a6

View on Github →

feat(topology/metric_space/holder): add holder_on_with (#8454)

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.tendsto_const_mul_rpow_nhds_zero_of_pos

Modified src/topology/metric_space/holder.lean

added theorem holder_on_with.comp

added theorem holder_on_with.comp_holder_with

added theorem holder_on_with.ediam_image_inter_le

added theorem holder_on_with.ediam_image_inter_le_of_le

added theorem holder_on_with.ediam_image_le

added theorem holder_on_with.ediam_image_le_of_le

added theorem holder_on_with.ediam_image_le_of_subset

added theorem holder_on_with.ediam_image_le_of_subset_of_le

added theorem holder_on_with.edist_le

added theorem holder_on_with.edist_le_of_le

added def holder_on_with

added theorem holder_on_with_empty

added theorem holder_on_with_one

added theorem holder_on_with_singleton

added theorem holder_on_with_univ

added theorem holder_with.comp_holder_on_with

added theorem set.subsingleton.holder_on_with

Modified src/topology/metric_space/lipschitz.lean

Modified src/topology/uniform_space/basic.lean

added theorem uniform_continuous_on_univ