extChartAt_target — Mathlib

English

The target of extChartAt I x is the preimage under I.symm of the chartAt H x target, intersected with the range of I.

Русский

Целевая область extChartAt I x равна предобразу симметрии I от целевой области chartAt H x, пересечённому с образом I.

LaTeX

$$$ (extChartAt I x).\\mathrm{target} = I^{\\mathrm{symm}-1}\\big((\\mathrm{chartAt} H x).\\mathrm{target}\\big) \\cap \\operatorname{range} I$$$

Lean4

theorem extChartAt_target (x : M) : (extChartAt I x).target = I.symm ⁻¹' (chartAt H x).target ∩ range I :=
  extend_target _

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