Mathlib Changelog
v4
Changelog
About
Github
Theorem
mulIndicator_cthickening_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_cthickening_eventually_eq_mulIndicator_closure
View on Github →