coe_extChartAt_transContinuousLinearEquiv_symm

English

The target set of extChartAt(I.transContinuousLinearEquiv e, x) equals the preimage of the original target under e: target ≡ e.symm^{-1}(target(extChartAt(I,x))).

Русский

Целевая область extChartAt(I.transContinuousLinearEquiv e, x) равна предобразу целевой области extChartAt(I,x) через e: целевая область = e^{-1}(target(extChartAt(I,x))).

LaTeX

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

Lean4

theorem coe_extChartAt_transContinuousLinearEquiv_symm (x : M) :
    ⇑(extChartAt (I.transContinuousLinearEquiv e) x).symm = (extChartAt I x).symm ∘ e.symm :=
  rfl

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