Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-19 06:53 1cfb97d5

View on Github →

feat(analysis/normed/group/pointwise): the closed thickening of a compact set is the addition of a closed ball. (#11528)

Estimated changes

Modified src/analysis/normed/group/pointwise.lean

added theorem is_compact.cthickening_eq_add_closed_ball

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem is_compact.cthickening_eq_bUnion_closed_ball

added theorem metric.closed_ball_subset_cthickening

added theorem metric.closed_ball_subset_cthickening_singleton

added theorem metric.cthickening_singleton

added theorem metric.thickening_singleton