contMDiff_pi_space — Mathlib

English

A function φ: M → ∏ Fi,i is ContMDiff iff all coordinate maps φ_i are ContMDiff.

Русский

Функция φ: M → ∏ Fi,i гладкая тогда и только тогда, когда все координаты φ_i гладкие.

LaTeX

$$$ ContMDiff I 𝓘(\mathbb{k}, ∀ i, Fi_i) n φ \iff \forall i, ContMDiff I 𝓘(\mathbb{k}, Fi_i) n (\lambda x. φ x i) $$$

Lean4

theorem contMDiff_pi_space : ContMDiff I 𝓘(𝕜, ∀ i, Fi i) n φ ↔ ∀ i, ContMDiff I 𝓘(𝕜, Fi i) n fun x => φ x i :=
  ⟨fun h i x => contMDiffAt_pi_space.1 (h x) i, fun h x => contMDiffAt_pi_space.2 fun i => h i x⟩

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