Theorem LipschitzOnWith.coordinate

Modification history

2023-06-18 00:43
Mathlib/Analysis/NormedSpace/lpSpace.lean
feat: Lipschitz extensions of maps into l^infty (#5107) …
Added LipschitzOnWith.coordinateView on Github →