differentiableWithinAt_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 x i is differentiable within t at y.

Русский

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

LaTeX

$$$$\\text{DifferentiableWithinAt } 𝕜 f t y \\iff \\forall i, \\text{DifferentiableWithinAt } 𝕜 (f\\cdot i) t y.$$$$

Lean4

theorem differentiableWithinAt_piLp :
    DifferentiableWithinAt 𝕜 f t y ↔ ∀ i, DifferentiableWithinAt 𝕜 (fun x => f x i) t y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableWithinAt_iff, differentiableWithinAt_pi]
  rfl

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