Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 23:48 7fec4014

View on Github →

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets (#10188) Add definition and basic API about open thickenings of subsets in metric spaces, in preparation for the portmanteau theorem on characterizations of weak convergence of Borel probability measures.

Estimated changes