Theorems · Definition · global analysis

ApproximatesLinearOn

{𝕜 : 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] → (E → F) → (E →L[𝕜] F) → Set E → NNReal → Prop

We say that f approximates a continuous linear map f' on s with constant c, if ‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖ whenever x, y ∈ s. This predicate is defined to facilitate the splitting of the inverse function theorem into small lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined on a specific set.

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Cited by

38 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace