writtenInExtChartAt_extChartAt — Mathlib

English

In a model where the base space is modeled on E, the extended chart at x coincides with the underlying model I when viewed as a map from E to E.

Русский

В модели, где базовое пространство моделируется на E, расширенная карта в точке x совпадает с базовой моделью I как отображение из E в E.

LaTeX

$$$\mathrm{extChartAt} 𝓘(\mathbb{K}, E) x = I$ as a map, i.e., extChartAt I x = I.$$

Lean4

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

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