Theorems · Theorem · functional analysis

lipschitzExtensionConstant_def

∀ (E' : Type u_1) [inst : NormedAddCommGroup E'] [inst_1 : NormedSpace ℝ E'] [inst_2 : FiniteDimensional ℝ E'],
  lipschitzExtensionConstant E' =
    have A := (Module.Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
    max (‖↑A.symm‖₊ * ‖↑A‖₊) 1

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional