contDiff_pi — Mathlib

English

A function Φ: E → ∀ i, F'_i is ContDiff 𝕜 n on s iff each coordinate Φ x i is ContDiff 𝕜 n on s.

Русский

Функция Φ: E → ∀ i, F'_i является ContDiff 𝕜 n на s тогда и только тогда каждая координата Φ x i является ContDiff 𝕜 n на s.

LaTeX

$$$ ContDiff 𝕜 n Φ \iff \forall i, ContDiff 𝕜 n (\\lambda x. Φ x i) $$$

Lean4

theorem contDiff_pi : ContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i := by
  simp only [← contDiffOn_univ, contDiffOn_pi]

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