mathlib

917b5275 - feat(topology/metric_space/thickened_indicator): Add definition and lemmas about thickened indicators. (#13481)