contDiff_pi'

Mathlib.Analysis.Calculus.ContDiff.Operations

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

English

The function x ↦ update x i is ContDiff for any index i and any order k.

Русский

Функция x ↦ update x i является ContDiff для любого i и любого порядка k.

LaTeX

$$$ ContDiff 𝕜 k (update x i) $$$

Lean4

@[fun_prop]
theorem contDiff_pi' (hΦ : ∀ i, ContDiff 𝕜 n fun x => Φ x i) : ContDiff 𝕜 n Φ :=
  contDiff_pi.2 hΦ

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

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

Разделы

Аффилиация

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