mem_achart_source

Mathlib.Geometry.Manifold.ChartedSpace

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

English

For every x, x lies in the source of the chart at x; i.e., x belongs to the domain where the chart is defined.

Русский

Для каждого x выполняется: x принадлежит области определения карты chartAt H x.

LaTeX

$$x \in (achart H x).1.source$$

Lean4

theorem mem_achart_source (x : M) : x ∈ (achart H x).1.source :=
  mem_chart_source H x

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

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

Разделы

Аффилиация

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