writtenInExtChartAt_model_space — Mathlib

English

For a model with corners I on E, the range of I is uniquely MDifferentiable, i.e., it carries a unique MDiffOn structure.

Русский

Для модели с краями I на E диапазон I обладает уникальной структурой MDifferentiable.

LaTeX

$$$\mathrm{MDiffOn}(\mathcal{I}_{𝕜,E}, \mathrm{range}(I))\;\text{ is unique.}$$$

Lean4

@[simp, mfld_simps]
theorem writtenInExtChartAt_model_space : writtenInExtChartAt 𝓘(𝕜, E) 𝓘(𝕜, E') x f = f :=
  rfl

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