contDiffAt_fst — Mathlib

English

If MapsTo f s t holds and g ∘ f is differentiable up to order n, then the i-th iterated derivative within s equals the Taylor composition up to i.

Русский

Если MapsTo f s t выполняется и g ∘ f гладко до порядка n, то i-я итеративная производная внутри s равна Taylor-композиции до i.

LaTeX

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

Lean4

/-- The first projection at a point in a product is `C^∞`. -/
@[fun_prop]
theorem contDiffAt_fst {p : E × F} : ContDiffAt 𝕜 n (Prod.fst : E × F → E) p :=
  contDiff_fst.contDiffAt

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