Theorem LipschitzOnWith.coordinate

Modification history

2026-03-30 20:46
Mathlib/Analysis/Normed/Lp/lpSpace.lean
feat: add missing API for `lp E p` (#35152) …
Modified LipschitzOnWith.coordinateView on Github →
2023-06-18 00:43
Mathlib/Analysis/NormedSpace/lpSpace.lean
feat: Lipschitz extensions of maps into l^infty (#5107) …
Added LipschitzOnWith.coordinateView on Github →