chartAt_self_eq

Mathlib.Geometry.Manifold.ChartedSpace

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

← MathLib Explorer

English

In model space, the chartAt map equals the identity chart.

Русский

В модельном пространстве chartAt совпадает с тождественной картой.

LaTeX

$$chartAt H x = OpenPartialHomeomorph.refl H$$

Lean4

/-- In the model space, `chartAt` is always the identity. -/
theorem chartAt_self_eq {H : Type*} [TopologicalSpace H] {x : H} : chartAt H x = OpenPartialHomeomorph.refl H :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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