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.