ApproximatesLinearOn.exists_homeomorph_extension

theorem ApproximatesLinearOn.exists_homeomorph_extension : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : FiniteDimensional ℝ F] {s : Set E} {f : E → F} {f' : E ≃L[ℝ] F} {c : NNReal}, ApproximatesLinearOn f (↑f') s c → Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹ → ∃ g, Set.EqOn f (⇑g) s

The theorem states that in the context of a real vector space, given a function `f` that approximates a linear equivalence `f'` on a subset `s` of the vector space `E` with nonnegative real number `c`, if `E` is a singleton or the product of the Lipschitz extension constant of `F` and `c` is less than the inverse of the norm of `f'.symm`, then there exists another function `g` such that `f` and `g` are equal on the subset `s`. This theorem essentially shows the ability to extend a function that approximates a linear equivalence on a subset, to a homeomorphism of the entire vector space.

More concisely: Given a real vector space `E`, a subset `s` of `E`, a function `f : s → E`, a linear equivalence `f' : E → E`, a nonnegative real number `c`, and a Lipschitz constant `K` for the extension of `f` to all of `E`, if `E` is a singleton or `K * c < 1 / ||f'.symm||`, then there exists a function `g : E → E` that agrees with `f` on `s` and is a homeomorphism of `E`.