union

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.RelCWComplex.union

English

The union of the base D with all closed cells equals C.

Русский

Объединение основания D с всеми замкнутыми клетками даёт C.

LaTeX

$$$D \cup \bigcup_{n, j} closedCell\; n\; j = C$$$

Lean4

theorem union [RelCWComplex C D] : D ∪ ⋃ (n : ℕ) (j : cell C n), closedCell n j = C :=
  RelCWComplex.union'

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

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

Разделы

Аффилиация

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