chart_source_mem_nhds

Mathlib.Geometry.Manifold.ChartedSpace

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

English

The source of the chart At x lies in the neighborhood of x.

Русский

Источник чарта At x лежит в окрестности x.

LaTeX

$$$(chartAt(H,x)).source \\in \\mathcal{N}(x)$$$

Lean4

theorem chart_source_mem_nhds (x : M) : (chartAt H x).source ∈ 𝓝 x :=
  (chartAt H x).open_source.mem_nhds <| mem_chart_source H x

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

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

Разделы

Аффилиация

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