Theorems · Definition · global analysis

ApproximatesLinearOn.toOpenPartialHomeomorph

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                (f : E → F) →
                  {f' : E ≃L[𝕜] F} →
                    (s : Set E) →
                      {c : NNReal} →
                        [CompleteSpace E] →
                          ApproximatesLinearOn f (↑f') s c →
                            Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → IsOpen s → OpenPartialHomeomorph E F

Given a function f that approximates a linear equivalence on an open set s, returns an open partial homeomorphism with toFun = f and source = s.

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Cited by

4 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpace