Commit 2023-07-26 06:04 3bbd2041

View on Github →

feat (Mathlib.Topology.MetricSpace.ThickenedIndicator): Add convergence of plain old indicators. (#6047) Add lemmas tendsto_indicator_thickening_indicator_closure and tendsto_indicator_cthickening_indicator_closure.

Estimated changes

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Metric.eventually_not_mem_cthickening_of_infEdist_pos

added theorem Metric.eventually_not_mem_thickening_of_infEdist_pos

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

added theorem mulIndicator_cthickening_eventually_eq_mulIndicator_closure

added theorem mulIndicator_thickening_eventually_eq_mulIndicator_closure

added theorem tendsto_mulIndicator_cthickening_mulIndicator_closure

added theorem tendsto_mulIndicator_thickening_mulIndicator_closure