mem_chart_source

Mathlib.Geometry.Manifold.ChartedSpace

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

← MathLib Explorer

English

The point x lies in the source of its chart At x.

Русский

Точка x принадлежит источнику chartAt(H,x).

LaTeX

$$$x \\in (chartAt(H,x)).source$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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