chart_mem_atlas

Mathlib.Geometry.Manifold.ChartedSpace

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

← MathLib Explorer

English

The chart at x belongs to the atlas of charts.

Русский

ЧартAt(H,x) принадлежит атласу диаграмм.

LaTeX

$$$chartAt(H,x) \\in atlas(H,M)$$$

Lean4

@[simp, mfld_simps]
theorem chart_mem_atlas (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
    chartAt H x ∈ atlas H M :=
  ChartedSpace.chart_mem_atlas x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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