extend_coord_change_source_mem_nhdsWithin'

English

For any x in the domain, the source of the composed extended maps lies inside a nhdsWithin neighborhood of x, provided the midpoint belongs to the range. This ensures local compatibility for chart changes.

Русский

Для любой x в области определения композиции расширенных карт источник лежит внутри nhdsWithin окрестности x, если диапазон содержит x.

LaTeX

$$$\\text{source}((f^{\\mathrm{ext}})^{-1} \\circ f'^{\\mathrm{ext}}) \\in 𝓝[\\mathrm{range}\\, I] x$$$

Lean4

theorem extend_coord_change_source_mem_nhdsWithin' {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
    ((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range I] f.extend I x :=
  by
  apply extend_coord_change_source_mem_nhdsWithin
  rw [← extend_image_source_inter]
  exact mem_image_of_mem _ ⟨hxf, hxf'⟩

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