extChartAt_model_space_eq_id — Mathlib

English

In the model-space case, extChartAt equals the identity on the base vector space; every extended chart acts as the identity.

Русский

В случае пространства модели extChartAt равна идентичности на базовом векторном пространстве; каждая расширенная карта есть идентичность.

LaTeX

$$extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E$$

Lean4

/-- In the case of the manifold structure on a vector space, the extended charts are just the
identity. -/
theorem extChartAt_model_space_eq_id (x : E) : extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E := by simp only [mfld_simps]

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