Theorem mulIndicator_thickening_eventually_eq_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 mulIndicator_thickening_eventually_eq_mulIndicator_closureView on Github →