fderivWithin_comp_of_eq — Mathlib

English

Variant of fderivWithin_comp with equality hy replaced by direct equality f(x) = y.

Русский

Вариант fderivWithin_comp с заменой равенства f(x) = y на прямое равенство.

LaTeX

$$$fderivWithin 𝕜 (g\circ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)$$$

Lean4

theorem fderivWithin_comp_of_eq {g : F → G} {t : Set F} {y : F} (hg : DifferentiableWithinAt 𝕜 g t y)
    (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t) (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
    fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x) := by subst hy;
  exact fderivWithin_comp _ hg hf h hxs

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