comp_contDiffWithinAt_of_eq — Mathlib

English

If g is ContDiffAt at y and f is ContDiffWithinAt at x with f(x)=y, then g ∘ f is ContDiffWithinAt at x.

Русский

Если g является ContDiffAt в точке y и f имеет ContDiffWithinAt в x с условием f(x)=y, то g ∘ f имеет ContDiffWithinAt в x.

LaTeX

$$$\forall x\in E,\; \ContDiffAt 𝕜 n g y \rightarrow \ContDiffWithinAt 𝕜 n f s x \rightarrow f x = y \rightarrow \ContDiffWithinAt 𝕜 n (g \circ f) s x$$$

Lean4

theorem comp_contDiffWithinAt_of_eq {y : F} (x : E) (hg : ContDiffAt 𝕜 n g y) (hf : ContDiffWithinAt 𝕜 n f s x)
    (hy : f x = y) : ContDiffWithinAt 𝕜 n (g ∘ f) s x := by subst hy; exact hg.comp_contDiffWithinAt x hf

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