extend_coord_change_source — Mathlib

English

The source of extChartAt equals the source of the standard chart at the point, reflecting that extending preserves the original domain of definition.

Русский

Область определения extChartAt совпадает с областью обычной карты в точке; расширение сохраняет исходную область.

LaTeX

$$$\\mathrm{source}(\\mathrm{extChartAt}(I,x)) = \\mathrm{source}(\\mathrm{chartAt} \\ H x)$$$

Lean4

theorem extend_coord_change_source : ((f.extend I).symm ≫ f'.extend I).source = I '' (f.symm ≫ₕ f').source :=
  by
  simp_rw [PartialEquiv.trans_source, I.image_eq, extend_source, PartialEquiv.symm_source, extend_target,
    inter_right_comm _ (range I)]
  rfl

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