extChartAt_transContinuousLinearEquiv_target

English

A simplified version of the target relation for extChartAt under a linear transport.

Русский

Упрощённая версия отношения целевой области для extChartAt при линейном переносе.

LaTeX

$$$\mathrm{target}\bigl(\mathrm{extChartAt}(I.transContinuousLinearEquiv e)\, x\bigr) = e^{-1}\bigl( \mathrm{target}(\mathrm{extChartAt}(I, x))\bigr)$$$

Lean4

theorem extChartAt_transContinuousLinearEquiv_target (x : M) :
    (extChartAt (I.transContinuousLinearEquiv e) x).target = e.symm ⁻¹' (extChartAt I x).target := by
  simp only [range_comp, preimage_preimage, ContinuousLinearEquiv.image_eq_preimage, mfld_simps, ← comp_def]

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