Theorem lipschitzWith_thickenedIndicator

Modification history

2025-10-10 14:40
Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
feat: `thickenedIndicator` is Lipschitz (#30346)
Added lipschitzWith_thickenedIndicatorView on Github →