differentiableAt_piLp — Mathlib

English

A function f: H → PiLp p E is differentiable at y if and only if each coordinate function f x i is differentiable at y.

Русский

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

LaTeX

$$$$\\text{DifferentiableAt } f y \\iff \\forall i, \\text{DifferentiableAt } (f\\cdot i) y.$$$$

Lean4

theorem differentiableAt_piLp : DifferentiableAt 𝕜 f y ↔ ∀ i, DifferentiableAt 𝕜 (fun x => f x i) y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableAt_iff, differentiableAt_pi]
  rfl

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