English
If hh₂ has derivative h₂′ at y, hf has derivative f′ on s at x, and y = f x with MapsTo condition to t, then the derivative within s of h₂ ∘ f at x equals h₂′ • f′.
Русский
Если hh₂ имеет производную h₂′ в y, hf имеет производную f′ на s в x, и y = f x с условием отображения, то производная внутри s композиции равна h₂′ • f′.
LaTeX
$$$$\\forall x:\\;\\text{hh₂: HasDerivWithinAt } h_2 h_2' t y \\land \\text{hf: HasFDerivWithinAt } f f' s x \\land \\text{MapsTo } f s t \\Rightarrow \\text{HasFDerivWithinAt}(h_2\\circ f) (h_2'\\cdot f') s x. $$$$
Lean4
theorem comp_hasDerivAt {t} (hh₂ : HasDerivWithinAt h₂ h₂' t (h x)) (hh : HasDerivAt h h' x)
(ht : ∀ᶠ x' in 𝓝 x, h x' ∈ t) : HasDerivAt (h₂ ∘ h) (h₂' * h') x :=
HasDerivAtFilter.comp x hh₂ hh <| tendsto_nhdsWithin_iff.mpr ⟨hh.continuousAt, ht⟩
