isOpen_extChartAt_source

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

For every x in M, the source of extChartAt I x is an open subset of M.

Русский

Для каждого x ∈ M множество-источник extChartAt I x является открытым.

LaTeX

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

Lean4

theorem isOpen_extChartAt_source (x : M) : IsOpen (extChartAt I x).source :=
  isOpen_extend_source _

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

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

Разделы

Аффилиация

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