mathlib

89fd6afc - feat(topology/metric_space/hausdorff_distance): A `cthickening` is an intersection of `thickenings` (#17258)

feat(topology/metric_space/hausdorff_distance): A `cthickening` is an intersection of `thickenings` (#17258) ... unconditionally. This is useful for me because being an upper set is a property that holds under unions, regardless of whether `0 ≤ δ` or not.