Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional

A lemma about ApproximatesLinearOn that needs FiniteDimensional #

In this file we prove that in a real vector space, a function f that approximates a linear equivalence on a subset s can be extended to a homeomorphism of the whole space.

This used to be the only lemma in Mathlib/Analysis/Calculus/Inverse depending on FiniteDimensional, so it was moved to a new file when the original file got split.

theorem ApproximatesLinearOn.exists_homeomorph_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] [FiniteDimensional F] {s : Set E} {f : EF} {f' : E ≃L[] F} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E lipschitzExtensionConstant F * c < f'.symm‖₊⁻¹) :
∃ (g : E ≃ₜ F), Set.EqOn f (⇑g) s

In a real vector space, a function f that approximates a linear equivalence on a subset s can be extended to a homeomorphism of the whole space.