Theorems · Theorem · functional analysis

LipschitzOnWith.extend_finite_dimension

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace ℝ E'] [inst_3 : FiniteDimensional ℝ E'] {s : Set α} {f : α → E'} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s

Any K-Lipschitz map from a subset s of a metric space α to a finite-dimensional real vector space E' can be extended to a Lipschitz map on the whole space α, with a slightly worse constant lipschitzExtensionConstant E' * K.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

1 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceNormedAddCommGroupNormedSpaceFiniteDimensional