Theorem LocallyLipschitzOn.exists_lipschitzOnWith_of_compact

Modification history

2025-12-23 12:27
Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean
feat: add ContDiff.lipschitzOnWith (#30612) …
Added LocallyLipschitzOn.exists_lipschitzOnWith_of_compactView on Github →