English
If p = p1 and u = u1, then the composed maps are congruent: p.compContinuousLinearMap u = p1.compContinuousLinearMap u1.
Русский
Если p = p1 и u = u1, то полученные композиции совпадают.
LaTeX
$$p = p1 → u = u1 → p.compContinuousLinearMap u = p1.compContinuousLinearMap u1$$
Lean4
/-- Data used to apply the generic implicit function theorem to the case of a strictly
differentiable map such that its derivative is surjective and has a complemented kernel. -/
@[simp]
def implicitFunctionDataOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
(hker : (ker f').ClosedComplemented) : ImplicitFunctionData 𝕜 E F (ker f')
where
leftFun := f
leftDeriv := f'
rightFun x := Classical.choose hker (x - a)
rightDeriv := Classical.choose hker
pt := a
left_has_deriv := hf
right_has_deriv := (Classical.choose hker).hasStrictFDerivAt.comp a ((hasStrictFDerivAt_id a).sub_const a)
left_range := hf'
right_range := LinearMap.range_eq_of_proj (Classical.choose_spec hker)
isCompl_ker := LinearMap.isCompl_of_proj (Classical.choose_spec hker)
