ImplicitFunctionData.hasStrictFDerivAt

theorem ImplicitFunctionData.hasStrictFDerivAt : ∀ {𝕜 : 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), HasStrictFDerivAt φ.prodFun (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)) φ.pt

The theorem `ImplicitFunctionData.hasStrictFDerivAt` states that for any scalar field 𝕜 (that is a nontrivial normed field), normed additive commutative groups E, F, and G (with E, F, and G also being complete normed spaces over 𝕜), and any Implicit Function Data φ, the function `ImplicitFunctionData.prodFun φ` has a strict Frechet derivative at the point φ.pt. The Frechet derivative is represented by the continuous linear map obtained by applying the function `ContinuousLinearMap.equivProdOfSurjectiveOfIsCompl` to φ's left and right derivatives.

More concisely: For any nontrivial normed field 𝕜 and Implicit Function Data φ over complete normed spaces E, F, and G, the function `ImplicitFunctionData.prodFun φ` has a strict Frechet derivative at φ.pt represented by the product of its left and right derivatives as continuous linear maps.