coordChangeL — Mathlib

English

The coordChangeL map is ContMDiff in the ambient differentiable structure; i.e., the fibre-coordinates transform smoothly with respect to the total space's differentiable structure.

Русский

Координатное преобразование гладко в общей дифференцируемой структуре пространства.

LaTeX

$$$\operatorname{ ContMDiff coordChangeL } \; := \dots$$$

Lean4

protected theorem coordChangeL (hf : ContMDiff IM IB n f) (he : ∀ x, f x ∈ e.baseSet) (he' : ∀ x, f x ∈ e'.baseSet) :
    ContMDiff IM 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) := fun x ↦
  (hf x).coordChangeL (he x) (he' x)

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