Commit 2022-01-20 07:43 e96e55d8

feat(analysis/normed_space/finite_dimension): extending partially defined Lipschitz functions (#11530) Any Lipschitz function on a subset of a metric space, into a finite-dimensional real vector space, can be extended to a globally defined Lipschitz function (up to worsening slightly the Lipschitz constant).