Theorems · Definition · global analysis

ImplicitFunctionData.implicitFunction

• 1000+ list: Implicit function theorem

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → F → G → E

Implicit function theorem. If f : E → F and g : E → G are two maps strictly differentiable at a, their derivatives f', g' are surjective, and the kernels of these derivatives are complementary subspaces of E, then implicitFunction is the unique (germ of a) map φ : F → G → E such that f (φ y z) = y and g (φ y z) = z.

Defined in

Mathlib.Analysis.Calculus.Implicit

Cited by

26 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpaceNormedAddCommGroupNormedSpaceCompleteSpace