contDiffWithinAt_extend_coord_change'

English

A variant of the previous differentiability result holds when restricting to a neighborhood in the target model space, showing the robustness of coordinate-change differentiability under extension.

Русский

Вариант предыдущего утверждения для ограниченной окрестности в целевом модельном пространстве демонстрирует устойчивость дифференцируемости перехода координат при расширении.

LaTeX

$$$\\text{ContDiffWithinAt}_{\\mathbb{K}, n} ( f^{\\mathrm{ext}} \\circ (f'.\\mathrm{ext})^{-1}, \\mathrm{range}\\, I, x)$$$

Lean4

theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) :=
  by
  refine contDiffWithinAt_extend_coord_change hf hf' ?_
  rw [← extend_image_source_inter]
  exact mem_image_of_mem _ ⟨hxf', hxf⟩

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