Commit 2023-07-31 08:03 275e357b

feat: generalize tendsto_measure_cthickening from PseudoMetricSpace to PseudoEMetricSpace and add corresponding lemmas for open thickenings (#6194) This PR mainly makes the generalization so that tendsto_measure_cthickening and tendsto_measure_cthickening_of_isClosed assume [PseudoEMetricSpace] instead of [PseudoMetricSpace] (the proofs require no changes, but the generality seems valuable). Also the counterparts tendsto_measure_thickening and tendsto_measure_thickening_of_isClosed for open thickenings (instead of closed thickenings) are added.