coordChange — Mathlib

English

Within a ContMDiffAt context, the coordChangeL map is ContMDiffWithinAt, respecting the base maps.

Русский

В рамках ContMDiffAt отображение coordChangeL гладко в пределах базовых отображений.

LaTeX

$$$\text{ContMDiffWithinAt coordChangeL}$$$

Lean4

protected nonrec theorem coordChange (hf : ContMDiffAt IM IB n f x) (hg : ContMDiffAt IM 𝓘(𝕜, F) n g x)
    (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
    ContMDiffAt IM 𝓘(𝕜, F) n (fun y ↦ e.coordChange e' (f y) (g y)) x :=
  hf.coordChange hg he he'

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