Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-26 07:55 1b1ae61f

View on Github →

feat(analysis/normed_space/pointwise): Thickening a thickening (#13380) In a real normed space, thickening twice is the same as thickening once.

Estimated changes

Modified src/analysis/normed_space/pointwise.lean

added theorem cthickening_cthickening

added theorem cthickening_thickening

added theorem inf_edist_cthickening

added theorem inf_edist_thickening

added theorem thickening_cthickening

added theorem thickening_thickening

Modified src/data/real/ennreal.lean

added theorem ennreal.le_sub_of_add_le_left

added theorem ennreal.le_sub_of_add_le_right

added theorem ennreal.of_real_sub

Modified src/topology/metric_space/basic.lean

added theorem edist_le_of_real

added theorem edist_lt_of_real

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem metric.cthickening_cthickening_subset

added theorem metric.cthickening_thickening_subset

added theorem metric.thickening_cthickening_subset

added theorem metric.thickening_thickening_subset