iUnion_openCell_eq_complex

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.CWComplex.iUnion_openCell_eq_complex

← MathLib Explorer

English

The union of all open cells equals the entire CW complex C.

Русский

Объединение всех открытых клеток равно всему CW-комплексу C.

LaTeX

$$$\bigcup_{n} \bigcup_{j} openCell (C := C) n j = C$$$

Lean4

theorem iUnion_openCell_eq_complex [CWComplex C] : ⋃ (n : ℕ) (j : cell C n), openCell n j = C := by
  simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C)

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

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

Разделы

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

Аффилиация

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