contDiffOn_extend_coord_change — Mathlib

English

If two charts f and f' belong to a maximal atlas, then the coordinate-change map between their extensions is differentiable on their common source. This shows smooth compatibility of the atlas with extensions.

Русский

Если карты f и f' входят в максимальный атлас, то переход координат между их продолжениями гладок на общей области определения. Это демонстрирует гладкую совместимость атласа и расширений.

LaTeX

$$$\\mathrm{ContDiffOn}_{\\mathbb{K}, n}\\big( f^{\\mathrm{ext}} \\circ (f'.\\mathrm{ext})^{-1}, \\mathrm{source} \\big)$$$

Lean4

theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) :
    ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source :=
  by
  rw [extend_coord_change_source, I.image_eq]
  exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1

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