hasFDerivAt_apply — Mathlib

English

For the i-th coordinate projection on PiLp p E, the derivative is the i-th projection map; in other words, the operation of taking the i-th component is differentiable with derivative equal to the projection.

Русский

Для i-й компоненты проекции на PiLp p E производная равна i-й проекции; операция извлечения i-й компоненты дифференцируема и производная равна проекции.

LaTeX

$$$ \text{HasFDerivAt}\big( f \mapsto f_i , \; \operatorname{proj}_i ,\; f\big) $$

Lean4

nonrec theorem hasFDerivAt_apply (f : PiLp p E) (i : ι) :
    HasFDerivAt (𝕜 := 𝕜) (fun f : PiLp p E => f i) (proj p E i) f :=
  (hasStrictFDerivAt_apply p f i).hasFDerivAt

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