contMDiffOn_pi_space — Mathlib

English

A function φ: M → ∏ Fi,i is ContMDiff on s iff every coordinate φ_i is ContMDiff on s.

Русский

Отображение φ: M → ∏ Fi,i гладко на s тогда и только тогда, когда каждая координата φ_i гладкая на s.

LaTeX

$$$ ContMDiffOn I 𝓘(\mathbb{k}, \{Fi_i\}) n \; \varphi\; s \iff \forall i, \ ContMDiffOn I 𝓘(\mathbb{k}, Fi_i) n (\lambda x. \varphi x i) s $$$

Lean4

theorem contMDiffOn_pi_space :
    ContMDiffOn I 𝓘(𝕜, ∀ i, Fi i) n φ s ↔ ∀ i, ContMDiffOn I 𝓘(𝕜, Fi i) n (fun x => φ x i) s :=
  ⟨fun h i x hx => contMDiffWithinAt_pi_space.1 (h x hx) i, fun h x hx =>
    contMDiffWithinAt_pi_space.2 fun i => h i x hx⟩

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