English
An alternative version of Subcomplex.mk with CW structure uses E and union similar to mk'.
Русский
Альтернативная версия Subcomplex.mk для CW используется E и объединение подобно mk'.
LaTeX
$$$$\text{mk'}:\; Subcomplex\,C$$$$
Lean4
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that for every cell of the subcomplex the corresponding closed cell is a subset of `E`. -/
@[simps! -isSimp]
def mk' [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : Π n, Set (cell C n))
(closedCell_subset : ∀ (n : ℕ) (i : I n), closedCell (C := C) n i ⊆ E)
(union : ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = E) : Subcomplex C :=
RelCWComplex.Subcomplex.mk' C E I closedCell_subset (by rw [empty_union]; exact union)
