derivWithin_clm_apply — Mathlib

English

The derivative of the function that picks a single coordinate i is the corresponding unit vector Pi.single i (1).

Русский

Производная функции выборки одной координаты i равна единичному вектору.

LaTeX

$$$HasDerivAt\\left(\\Pi.single\\, i\\right)\\left(\\Pi.single\\, i\\,(1 : 𝕜)\\right) y$$$

Lean4

theorem derivWithin_clm_apply (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
    derivWithin (fun y => (c y) (u y)) s x = derivWithin c s x (u x) + c x (derivWithin u s x) :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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