Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.bounded.thickening

Modification history

2021-12-18 20:11

src/topology/metric_space/hausdorff_distance.lean

feat(topology/metric/hausdorff_distance): more properties of cthickening (#10808)

Added metric.bounded.thickening View on Github →