contDiffAt_piLp' — Mathlib

English

If all coordinate projections are ContDiffWithinAt, then the whole map is ContDiffWithinAt.

Русский

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

LaTeX

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

Lean4

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

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