chart_mem_maximalAtlas

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#StructureGroupoid.chart_mem_maximalAtlas

English

For every x ∈ M, the chartAt H x belongs to the maximal atlas of G.

Русский

Для каждого x ∈ M карта chartAt H x принадлежит к максимальному атласу G.

LaTeX

$$$chartAt\ H\ x \in StructureGroupoid.maximalAtlas M G$$$

Lean4

theorem chart_mem_maximalAtlas [HasGroupoid M G] (x : M) : chartAt H x ∈ G.maximalAtlas M :=
  G.subset_maximalAtlas (chart_mem_atlas H x)

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

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

Разделы

Аффилиация

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