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.