English
Let E be a Subcomplex of a RelCWComplex C D. Then E is the union of the base D and all its closed cells: D ∪ ⋃_{n, j ∈ E.I(n)} closedCell(C := C) n j = E.
Русский
Пусть E — подкомплекс RelCWComplex C D. Тогда E является объединением базового множества D и всех его замкнутых клеток: D ∪ ⋃_{n, j ∈ E.I(n)} closedCell(C := C) n j = E.
LaTeX
$$$D \cup \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 and its base. -/
theorem union_closedCell [T2Space X] [RelCWComplex C D] (E : Subcomplex C) :
D ∪ ⋃ (n : ℕ) (j : E.I n), closedCell (C := C) n j = E :=
by
apply subset_antisymm
· apply union_subset E.base_subset
exact iUnion₂_subset fun n i ↦ closedCell_subset_of_mem E i.2
· rw [← E.union]
apply union_subset_union_right
apply iUnion₂_mono fun n i ↦ ?_
exact openCell_subset_closedCell (C := C) n i
