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 : E → F}
{f' : E ≃L[ℝ] F}
{c : NNReal}
(hf : ApproximatesLinearOn f (↑f') s c)
(hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹)
:
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.