writtenInExtChartAt_extChartAt_symm

English

The extended chart on a product space M × M' is the product of the extended charts on each factor.

Русский

Расширенная карта на произведении пространства M × M' является произведением расширенных карт на каждом факторе.

LaTeX

$$$\mathrm{extChartAt} (I.\mathrm{prod} I') (x,y) = (\mathrm{extChartAt} I x) \;\mathrm{prod} \; (\mathrm{extChartAt} I' y).$$$

Lean4

theorem writtenInExtChartAt_extChartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y := by simp_all only [mfld_simps]

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