comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem comp {g : F → G} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : DifferentiableWithinAt 𝕜 f s x)
    (h : MapsTo f s t) : DifferentiableWithinAt 𝕜 (g ∘ f) s x :=
  (hg.hasFDerivWithinAt.comp x hf.hasFDerivWithinAt h).differentiableWithinAt

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