extChartAt_self_eq

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

URI: https://scilib.ai/kg/mathlib#extChartAt_self_eq

English

In the model space case, extChartAt equals the identity chart, i.e., extChartAt 𝓘(𝕜,E) x = PartialEquiv.refl E.

Русский

В случае пространства модели extChartAt равна тождественной карте: extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E.

LaTeX

$$$extChartAt 𝓘(\mathbb{K}, E) x = \mathrm{PartialEquiv.refl} E$.$$

Lean4

theorem extChartAt_self_eq {x : H} : ⇑(extChartAt I x) = I :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru