Theorems · Definition · functional analysis

lipschitzExtensionConstant

(E' : Type u_1) → [inst : NormedAddCommGroup E'] → [inst_1 : NormedSpace ℝ E'] → [FiniteDimensional ℝ E'] → NNReal

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 C * K where C only depends on E'. We record a working value for this constant C as lipschitzExtensionConstant E'.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional