extend_coord_change_source_mem_nhdsWithin

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

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