hausdorff_distance): The diameter of a thickening (#17021)

Commit

3 years ago

feat(topology/metric_space/hausdorff_distance): The diameter of a thickening (#17021) The diameter of the `ε`-thickening of `s` is at most the diameter of `s` + `2ε`

Author

YaelDillies

Parents

d240ffbd

mathlib 08aeb33b - feat(topology/metric_space/hausdorff_distance): The diameter of a thickening (#17021)

mathlib
08aeb33b - feat(topology/metric_space/hausdorff_distance): The diameter of a thickening (#17021)