comp_contDiffWithinAt — Mathlib

English

Under the same hypotheses as above, the i-th iterated derivative within s satisfies the same Taylor composition equality.

Русский

При тех же условиях справедливо то же равенство для i-й итеративной производной внутри s.

LaTeX

$$$\forall i,\; \operatorname{iteratedFDerivWithin} 𝕜 i (g \circ f) s x = (\ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (\ftaylorSeriesWithin 𝕜 f s x) i$$$

Lean4

theorem comp_contDiffWithinAt {g : F → G} {f : E → F} (h : ContDiff 𝕜 n g) (hf : ContDiffWithinAt 𝕜 n f t x) :
    ContDiffWithinAt 𝕜 n (g ∘ f) t x :=
  haveI : ContDiffWithinAt 𝕜 n g univ (f x) := h.contDiffAt.contDiffWithinAt
  this.comp x hf (subset_univ _)

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