iUnion_source_chartAt

Mathlib.Geometry.Manifold.ChartedSpace

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

← MathLib Explorer

English

The union over all x in M of the sources of chartAt(H,x) equals the whole space M.

Русский

Объединение источников chartAt(H,x) по всем x из M равно M.

LaTeX

$$$\\bigcup_{x\\in M} (chartAt(H,x)).source = U$$

Lean4

@[simp]
theorem iUnion_source_chartAt : (⋃ x : M, (chartAt H x).source) = (univ : Set M) :=
  eq_univ_iff_forall.mpr fun x ↦ mem_iUnion.mpr ⟨x, mem_chart_source H x⟩

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

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

Разделы

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

Аффилиация

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