Theorems · Inductive type · global analysis

ImplicitFunctionData

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            (F : Type u_3) →
              [inst_4 : NormedAddCommGroup F] →
                [NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    (G : Type u_4) →
                      [inst_7 : NormedAddCommGroup G] →
                        [NormedSpace 𝕜 G] → [CompleteSpace G] → Type (max (max u_2 u_3) u_4)

Data for the general version of the implicit function theorem. It holds two functions f : E → F and g : E → G (named leftFun and rightFun) and a point a (named pt) such that * both functions are strictly differentiable at a; * the derivatives are surjective; * the kernels of the derivatives are complementary subspaces of E.

Defined in

Mathlib.Analysis.Calculus.Implicit

Cited by

44 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpace