contDiffWithinAt_piLp' — Mathlib

English

If each component f_i is ContDiffWithinAt, then f itself is ContDiffWithinAt.

Русский

Если каждая компонента f_i является ContDiffWithinAt, то сама функция f является ContDiffWithinAt.

LaTeX

$$$ (\forall i, ContDiffWithinAt\ 𝕜 n (f \cdot i) t y) \Rightarrow ContDiffWithinAt\ 𝕜 n f t y $$$

Lean4

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

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