English
Let hh₂ be differentiable at h(x) with derivative h₂′, hh be differentiable at x with derivative h′, and L′ be a filter such that h x converges along L to h x and Tendsto h L L′. Then the derivative of h₂ ∘ h at x along L is h₂′ times h′.
Русский
Пусть hh₂ дифференцируема в h(x) с производной h₂′, hh дифференцируема в x с производной h′, и имеет место переход по фильтру L. Тогда производная h₂ ∘ h в x по фильтру L равна произведению h₂′ на h′.
LaTeX
$$$$\\forall x\\;\\text{hh₂: HasDerivAtFilter } h₂ h₂' (h x) \;\\land\\; \\text{hh: HasDerivAtFilter } h h' x \;\\land\\; \\text{Filter.Tendsto } h L L' \\Rightarrow \\text{HasDerivAtFilter } (h_2\\circ h) (h_2' * h') x L. $$$$
Lean4
theorem comp_hasFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {t} (x) (hh : HasDerivWithinAt h₂ h₂' t y)
(hf : HasFDerivAt f f' x) (ht : ∀ᶠ x' in 𝓝 x, f x' ∈ t) (hy : y = f x) : HasFDerivAt (h₂ ∘ f) (h₂' • f') x := by
subst y; exact hh.comp_hasFDerivAt x hf ht
