Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Inverse function theorem, C^r case #

In this file we specialize the inverse function theorem to C^r-smooth functions.

def ContDiffAt.toOpenPartialHomeomorph {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] (f : EF) {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :

Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, returns an OpenPartialHomeomorph with to_fun = f and a ∈ source.

Equations
Instances For
    @[deprecated ContDiffAt.toOpenPartialHomeomorph (since := "2025-08-29")]
    def ContDiffAt.toPartialHomeomorph {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] (f : EF) {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :

    Alias of ContDiffAt.toOpenPartialHomeomorph.


    Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, returns an OpenPartialHomeomorph with to_fun = f and a ∈ source.

    Equations
    Instances For
      @[simp]
      theorem ContDiffAt.toOpenPartialHomeomorph_coe {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      (toOpenPartialHomeomorph f hf hf' hn) = f
      @[deprecated ContDiffAt.toOpenPartialHomeomorph_coe (since := "2025-08-29")]
      theorem ContDiffAt.toPartialHomeomorph_coe {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      (toOpenPartialHomeomorph f hf hf' hn) = f

      Alias of ContDiffAt.toOpenPartialHomeomorph_coe.

      theorem ContDiffAt.mem_toOpenPartialHomeomorph_source {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      @[deprecated ContDiffAt.mem_toOpenPartialHomeomorph_source (since := "2025-08-29")]
      theorem ContDiffAt.mem_toPartialHomeomorph_source {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :

      Alias of ContDiffAt.mem_toOpenPartialHomeomorph_source.

      theorem ContDiffAt.image_mem_toOpenPartialHomeomorph_target {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      @[deprecated ContDiffAt.image_mem_toOpenPartialHomeomorph_target (since := "2025-08-29")]
      theorem ContDiffAt.image_mem_toPartialHomeomorph_target {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :

      Alias of ContDiffAt.image_mem_toOpenPartialHomeomorph_target.

      def ContDiffAt.localInverse {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      FE

      Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, returns a function that is locally inverse to f.

      Equations
      Instances For
        theorem ContDiffAt.localInverse_apply_image {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
        hf.localInverse hf' hn (f a) = a
        theorem ContDiffAt.to_localInverse {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
        ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

        Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, the inverse function (produced by ContDiff.toOpenPartialHomeomorph) is also ContDiff.