contDiffAt_piLp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem contDiffAt_piLp : ContDiffAt 𝕜 n f y ↔ ∀ i, ContDiffAt 𝕜 n (fun x => f x i) y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffAt_iff, contDiffAt_pi]
  rfl

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