writtenInExtChartAt_chartAt_symm — Mathlib

English

For manifold structure with a Local chart, the coordinate change extChartAt I x between x and x' is C^n on its source.

Русский

Для локальной карты класса координат переход между точками x и x' является гладким класса C^n на своей области определения.

LaTeX

$$$\text{ContDiffOn}_{\mathbb{K}}^n(\mathrm{extChartAt} I x \circ (\mathrm{extChartAt} I x').symm) (((\mathrm{extChartAt} I x').symm \circ \mathrm{extChartAt} I x).\text{source})$$$

Lean4

theorem writtenInExtChartAt_chartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I (chartAt H x x) (chartAt H x).symm y = y := by simp_all only [mfld_simps]

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