chart_mem_maximalAtlas

Mathlib.Geometry.Manifold.IsManifold.Basic

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

English

For every x in M, the chartAt H x lies in the maximal atlas for the C^n structure on M.

Русский

Для каждого x в M диаграмма chartAt H x принадлежит максимальному атласу для структуры C^n на M.

LaTeX

$$chartAt(H,x) ∈ maximalAtlas(I,n,M)$$

Lean4

theorem chart_mem_maximalAtlas [IsManifold I n M] (x : M) : chartAt H x ∈ maximalAtlas I n M :=
  StructureGroupoid.chart_mem_maximalAtlas _ x

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

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

Разделы

Аффилиация

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