English
The derivative of a coordinate change between two charts is C^n on its source.
Русский
Производная перехода координат между двумя диаграммами является C^n на области определения.
LaTeX
$$$$ ContDiffOn\, 𝕜\, n\, \big( fderivWithin\ 𝕜\ (j.1.extend I \circ (i.1.extend I).symm) (range I) \big) \big((i.1.extend I).\mathrm{symm} \circ j.1.extend I\big).\mathrm{source} $$$$
Lean4
/-- Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is
`C^n` on its source. -/
theorem contDiffOn_fderiv_coord_change [IsManifold I (n + 1) M] (i j : atlas H M) :
ContDiffOn 𝕜 n (fderivWithin 𝕜 (j.1.extend I ∘ (i.1.extend I).symm) (range I))
((i.1.extend I).symm ≫ j.1.extend I).source :=
by
have h : ((i.1.extend I).symm ≫ j.1.extend I).source ⊆ range I := by rw [i.1.extend_coord_change_source];
apply image_subset_range
intro x hx
refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl <| h hx).mono h
refine
(OpenPartialHomeomorph.contDiffOn_extend_coord_change (subset_maximalAtlas j.2) (subset_maximalAtlas i.2) x
hx).mono_of_mem_nhdsWithin
?_
exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 hx
