union_closedCell — Mathlib

English

A subcomplex of a CW complex C is the union of its closed cells: ⋃_{n ∈ ℕ} ⋃_{j ∈ E.I(n)} closedCell(C,n,j) = E.

Русский

Подкомплекс CW-комплекса C равен объединению всех его замкнутых клеток: ⋃_{n ∈ ℕ} ⋃_{j ∈ E.I(n)} closedCell(C,n,j) = E.

LaTeX

$$$\bigcup_{n \in \mathbb{N}} \bigcup_{j \in E.I(n)} closedCell(C := C)\ n\ j = E$$$

Lean4

/-- A subcomplex is the union of its closed cells. -/
theorem union_closedCell [T2Space X] [CWComplex C] (E : Subcomplex C) :
    ⋃ (n : ℕ) (j : E.I n), closedCell (C := C) n j = E :=
  (empty_union _).symm.trans (RelCWComplex.Subcomplex.union_closedCell E)

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