contDiffOn_pi' — Mathlib

English

For any finite index set, the map Pi.single i is ContDiff 𝕜 k from F'_i to the space of all coordinate maps.

Русский

Для конечного множества индексов отображение Pi.single i непрерывно дифференцируемо 𝕜 k как отображение из F'_i в пространство всех координат.

LaTeX

$$$ ContDiff 𝕜 k (Pi.single i : F' i → ∀ i, F' i) $$$

Lean4

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

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