fun_comp' — Mathlib

English

If hg is differentiable at f(x) within t and hf is differentiable within s at x, then the composition is differentiable within s ∩ f^{-1}(t) at x.

Русский

Если hg дифференцируемо внутри t в f(x) и hf дифференцируемо внутри s в x, то композиция дифференцируема внутри s ∩ f^{-1}(t) в x.

LaTeX

$$$\text{DifferentiableWithinAt}_{𝕜} (g\circ f) (s \cap f^{-1}(t)) x$$$

Lean4

@[fun_prop]
theorem fun_comp' {f : E → F} {g : F → G} (hg : DifferentiableAt 𝕜 g (f x)) (hf : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜 (fun x ↦ g (f x)) x :=
  (hg.hasFDerivAt.comp x hf.hasFDerivAt).differentiableAt

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