mem_chart_target

Mathlib.Geometry.Manifold.ChartedSpace

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

English

The chart maps the point x to its value chartAt(H,x)(x); this lies in the target of the chart.

Русский

Чарт отображает точку x в chartAt(H,x)(x); это лежит в цели чарта.

LaTeX

$$$(chartAt(H,x))(x) \\in (chartAt(H,x)).target$$$

Lean4

theorem mem_chart_target (x : M) : chartAt H x x ∈ (chartAt H x).target :=
  (chartAt H x).map_source (mem_chart_source _ _)

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

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

Разделы

Аффилиация

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