contDiffOn_piLp' — Mathlib

English

If for all coordinates i the function f_i is ContDiffOn, then f is ContDiffOn.

Русский

Если для всех координат i функция f_i является ContDiffOn, то и f является ContDiffOn.

LaTeX

$$$ (\forall i, ContDiffOn\ 𝕜 n (f \mapsto f i) t) \Rightarrow ContDiffOn\ 𝕜 n f t $$$

Lean4

@[fun_prop]
theorem contDiffOn_piLp' (hf : ∀ i, ContDiffOn 𝕜 n (fun x => f x i) t) : ContDiffOn 𝕜 n f t :=
  (contDiffOn_piLp p).2 hf

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