Mathlib Changelog
v4
Changelog
About
Github
Theorem
LipschitzWith.coordinate
Modification history
2023-06-18 00:43
Mathlib/Analysis/NormedSpace/lpSpace.lean
feat: Lipschitz extensions of maps into l^infty (#5107) …
Added
LipschitzWith.coordinate
View on Github →