coe_extChartAt_transContinuousLinearEquiv

English

For every x, the extended chart of the transported model equals the composition of the linear isomorphism with the extended chart of the original model: extChartAt(I.transContinuousLinearEquiv e, x) = e ∘ extChartAt(I, x).

Русский

Для каждого узла x расширенная карта модели преобразованного по линейному изоморфизму равна композиции c линейным изоморфизмом с расширенной картой исходной модели.

LaTeX

$$$\mathrm{extChartAt}(I.transContinuousLinearEquiv e, x) = e \circ \mathrm{extChartAt}(I, x)$$$

Lean4

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

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