English
The derivative of the mapped implicit function equals the restriction map to ker f'; i.e., the differential of the implicit image is given by the kernel inclusion map.
Русский
Дифференциал полученной неявной функции соответствует ограничению на ker f'; то есть дифференциал образа неявной функции задаётся вложением ядра.
LaTeX
$$$ \text{to_implicitFunctionOfComplemented}(hf, hf', hker) : \ HasStrictFDerivAt \,(f a) \to (\ker f').subtypeL 0 $$$
Lean4
theorem to_implicitFunctionOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
(hker : (ker f').ClosedComplemented) :
HasStrictFDerivAt (hf.implicitFunctionOfComplemented f f' hf' hker (f a)) (ker f').subtypeL 0 :=
by
convert (implicitFunctionDataOfComplemented f f' hf hf' hker).implicitFunction_hasStrictFDerivAt (ker f').subtypeL _ _
swap
· ext
simp only [Classical.choose_spec hker, implicitFunctionDataOfComplemented, ContinuousLinearMap.comp_apply,
Submodule.coe_subtypeL', Submodule.coe_subtype, ContinuousLinearMap.id_apply]
swap
· ext
simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL', Submodule.coe_subtype, LinearMap.map_coe_ker,
ContinuousLinearMap.zero_apply]
simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]
