comp — Mathlib

English

If g is differentiable at f(x) and f is differentiable within s at x, then g∘f is differentiable within s at x.

Русский

Если g дифференцируемо в f(x) и f дифференцируемо внутри s в x, то g∘f дифференцируемо внутри s в x.

LaTeX

$$$\text{DifferentiableWithinAt}_{𝕜} (g\circ f) s x$$$

Lean4

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

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