contDiffWithinAt_piLp_apply — Mathlib

English

The differentiability of a finite product PiLp at a point is equivalent to the differentiability of each projection coordinate.

Русский

Дифференцируемость функции, принимающей значения в продукте PiLp, эквивалентна дифференцируемости каждой координаты проекции.

LaTeX

$$$ ContDiffAt\ 𝕜 n f y \Leftrightarrow \forall i,\ ContDiffAt\ 𝕜 n (f \mapsto f_i) y $$$

Lean4

@[fun_prop]
theorem contDiffWithinAt_piLp_apply {i : ι} {t : Set (PiLp p E)} {y : PiLp p E} :
    ContDiffWithinAt 𝕜 n (fun f : PiLp p E => f i) t y :=
  (contDiffWithinAt_piLp p).1 contDiffWithinAt_id i

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