comp_differentiableWithinAt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem comp_differentiableWithinAt {g : F → G} (hg : DifferentiableAt 𝕜 g (f x))
    (hf : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 (g ∘ f) s x :=
  hg.differentiableWithinAt.comp x hf (mapsTo_univ _ _)

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