comp_of_tendsto — Mathlib

English

If HasFDerivWithinAt for g at f(x) and HasFDerivWithinAt for f at x, and f tends to t through s, then HasFDerivWithinAt for the composition g ∘ f holds within s.

Русский

Если существуют внутри-производные для g и f и f стремится к x, то композиция g∘f имеет внутри-производную.

LaTeX

$$$\text{HasFDerivWithinAt} (g\circ f) s x = \text{HasFDerivWithinAt} g (g' ) t (f x) \circ f'$$

Lean4

@[fun_prop]
theorem comp_of_tendsto {g : F → G} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x))
    (hf : HasFDerivWithinAt f f' s x) (hst : Tendsto f (𝓝[s] x) (𝓝[t] f x)) :
    HasFDerivWithinAt (g ∘ f) (g'.comp f') s x :=
  HasFDerivAtFilter.comp x hg hf hst

Похожие утверждения