Commit 2025-10-10 14:40 e978dd5d

View on Github →

feat: thickenedIndicator is Lipschitz (#30346)

Estimated changes

Modified Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.sub_sub_sub_cancel_left

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

added theorem lipschitzWith_thickenedIndicator

added theorem thickenedIndicatorAux_mono_infEdist

added theorem thickenedIndicator_mono_infEdist