English
For a function φ: M → ∏_i Fi,i, ContMDiffWithinAt on a pi-space is equivalent to the family of ContMDiffWithinAt on each coordinate.
Русский
Для функции φ: M → ∏_i Fi,i гладкость ContMDiffWithinAt на Pi-пространстве эквивалентна тому, что каждая координата φ_i гладка на соответствующем факторе Fi,i.
LaTeX
$$$ ContMDiffWithinAt I \mathcal{I}(\mathbb{k}, \{Fi_i\}) n \; \varphi\; s\; x \;\Leftrightarrow\; \forall i, \ ContMDiffWithinAt I \mathcal{I}(\mathbb{k}, Fi_i) n (\lambda x. \varphi x i) s x $$$
Lean4
theorem contMDiffWithinAt_pi_space :
ContMDiffWithinAt I 𝓘(𝕜, ∀ i, Fi i) n φ s x ↔ ∀ i, ContMDiffWithinAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) s x := by
simp only [contMDiffWithinAt_iff, continuousWithinAt_pi, contDiffWithinAt_pi, forall_and,
extChartAt_model_space_eq_id, Function.comp_def, PartialEquiv.refl_coe, id]
