English
The hasFDerivAtFilter criterion is equivalent to a limit condition: the derivative is characterized by a tends-to-zero condition after rescaling by the inverse norm of x' - x.
Русский
Условие hasFDerivAtFilter эквивалентно условию предела: производная задаётся через предел, смещённый и нормировать на обратную норму (x' - x).
LaTeX
$$$\\text{HasFDerivAtFilter } f f' x L \\iff \\mathrm{Tendsto}\\ (\\lambda x',. )\\ L (\\nhds 0)$$$
Lean4
@[fun_prop]
theorem clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
HasFDerivAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x :=
by
-- `by exact` to solve unification issues.
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp x <| hc.prodMk hd
