2023-07-31 08:03
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: generalize tendsto_measure_cthickening from PseudoMetricSpace to PseudoEMetricSpace and add corresponding lemmas for open thickenings (#6194) …
Added tendsto_measure_thickening_of_isClosed