contDiff_piLp'

Mathlib.Analysis.Calculus.ContDiff.WithLp

URI: https://scilib.ai/kg/mathlib#contDiff_piLp'

English

If all coordinates are ContDiff, then f is ContDiff.

Русский

Если все координаты ContDiff, тогда f является ContDiff.

LaTeX

$$$ (\forall i, ContDiff\ 𝕜 n (fun x => f x i)) \Rightarrow ContDiff 𝕜 n f $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru