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 < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹) : ∃ (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.