English
The coordinate-change obtained by composing extended charts equals the transitive extension of the coordinate-change maps; this expresses the compatibility of extended charts with coordinate changes.
Русский
Координатные переходы, полученные через расширенные карты, равны композиции расширений переходов; это описывает совместимость расширенных карт и переходов координат.
LaTeX
$$$(f.extend I) \\circ (f'.extend I)^{-1}$ is compatible with extChartAt; i.e. its source equals the appropriate image under extension.$$
Lean4
theorem extend_coord_change_source_mem_nhdsWithin {x : E} (hx : x ∈ ((f.extend I).symm ≫ f'.extend I).source) :
((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] x :=
by
rw [f.extend_coord_change_source] at hx ⊢
obtain ⟨x, hx, rfl⟩ := hx
refine I.image_mem_nhdsWithin ?_
exact (OpenPartialHomeomorph.open_source _).mem_nhds hx