contDiffOn_piLp — Mathlib

English

A function on a domain to a product PiLp is ContDiffOn if and only if each coordinate projection is ContDiffOn.

Русский

Функция на области в продукте PiLp является ContDiffOn тогда и только тогда, когда каждая координатная проекция является ContDiffOn.

LaTeX

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

Lean4

theorem contDiffOn_piLp : ContDiffOn 𝕜 n f t ↔ ∀ i, ContDiffOn 𝕜 n (fun x => f x i) t :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]
  rfl

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