contDiff_piLp — Mathlib

English

A function into a PiLp space is ContDiff if and only if all coordinate projections are ContDiff.

Русский

Функция в пространство PiLp является ContDiff тогда и только тогда, когда все координатные проекции являются ContDiff.

LaTeX

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

Lean4

theorem contDiff_piLp : ContDiff 𝕜 n f ↔ ∀ i, ContDiff 𝕜 n fun x => f x i :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]
  rfl

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