Theorem tendsto_mulIndicator_thickening_mulIndicator_closure

Modification history

2023-07-26 06:04
Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
feat (Mathlib.Topology.MetricSpace.ThickenedIndicator): Add convergence of plain old indicators. (#6047) …
Added tendsto_mulIndicator_thickening_mulIndicator_closureView on Github →