extChartAt_source_mem_nhds

Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

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

English

The source of extChartAt I x is a neighborhood of x.

Русский

Область определения extChartAt I x является окрестностью x.

LaTeX

$$$ (extChartAt I x).source \\in 𝓝 x$$$

Lean4

theorem extChartAt_source_mem_nhds (x : M) : (extChartAt I x).source ∈ 𝓝 x :=
  extChartAt_source_mem_nhds' (mem_extChartAt_source x)

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

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

Разделы

Аффилиация

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