mathlib3

e96e55d8 - feat(analysis/normed_space/finite_dimension): extending partially defined Lipschitz functions (#11530)

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).