English
The map tangentCoordChange I x y is continuous on the intersection of chart sources.
Русский
Карта tangentCoordChange I x y непрерывна на пересечении источников диаграмм.
LaTeX
$$$$ \text{ContinuousOn}\big(\mathrm{tangentCoordChange} I x y\big)\big((\mathrm{extChartAt} I x).source \cap (\mathrm{extChartAt} I y).source\big) $$$$
Lean4
theorem hasFDerivWithinAt_tangentCoordChange {x y z : M} (h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source) :
HasFDerivWithinAt ((extChartAt I y) ∘ (extChartAt I x).symm) (tangentCoordChange I x y z) (range I)
(extChartAt I x z) :=
have h' : extChartAt I x z ∈ ((extChartAt I x).symm ≫ (extChartAt I y)).source :=
by
rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target]
exact mem_image_of_mem _ h
((contDiffWithinAt_ext_coord_change y x h').differentiableWithinAt le_rfl).hasFDerivWithinAt
