mem_extChartAt_source

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

The point x lies in the source of extChartAt I x.

Русский

Точка x принадлежит области определения extChartAt I x.

LaTeX

$$$ x \\in (\\mathrm{extChartAt}\\ I\\ x).\\mathrm{source}$$$

Lean4

theorem mem_extChartAt_source (x : M) : x ∈ (extChartAt I x).source := by
  simp only [extChartAt_source, mem_chart_source]

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

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

Разделы

Аффилиация

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