contMDiffAt_pi_space — Mathlib

English

A pointwise version: ContMDiffAt for a pi-space is equivalent to each coordinate ContMDiffAt.

Русский

Локальная гладкость в точке на пи-пространстве эквивалентна гладкости каждой координаты.

LaTeX

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

Lean4

theorem contMDiffAt_pi_space :
    ContMDiffAt I 𝓘(𝕜, ∀ i, Fi i) n φ x ↔ ∀ i, ContMDiffAt I 𝓘(𝕜, Fi i) n (fun x => φ x i) x :=
  contMDiffWithinAt_pi_space

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