contDiffAt_pi'

Mathlib.Analysis.Calculus.ContDiff.Operations

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

English

The map f ↦ f i from ι → E is ContDiff 𝕜 n for any fixed i.

Русский

Отображение f ↦ f i с фиксированным i является ContDiff 𝕜 n.

LaTeX

$$$ ContDiff 𝕜 n (fun f : ι → E => f i) $$$

Lean4

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

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

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

Разделы

Аффилиация

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