contDiffWithinAt_piLp — Mathlib

English

A function f: H → PiLp p E is differentiable within a set t at y if and only if each coordinate function f_i is differentiable within t at y.

Русский

Функция f: H → PiLp p E является внутри области t дифференцируемой в точке y тогда и только тогда, когда каждая координатная функция f_i дифференцируема внутри t в y.

LaTeX

$$$ ContDiffWithinAt\ 𝕜 n f t y \Leftrightarrow \forall i,\ ContDiffWithinAt\ 𝕜 n (\lambda x. f x i) t y $$$

Lean4

theorem contDiffWithinAt_piLp : ContDiffWithinAt 𝕜 n f t y ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => f x i) t y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffWithinAt_iff, contDiffWithinAt_pi]
  rfl

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