English
Let C be a CW complex and X a T2 space. For any A ⊆ X and n ∈ ℕ, if for every m ≤ n and every j ∈ cell C m we have A ∩ closedCell m j is closed, then for every j ∈ cell C (n+1), A ∩ cellFrontier (n+1) j is closed.
Русский
Пусть C — CW-комплекс и X — т1-пространство. Для любого A ⊆ X и n ∈ ℕ, если для каждого m ≤ n и каждой клетки j ∈ cell C m верно, что A ∩ closedCell m j замкнуто, то для каждого j ∈ cell C (n+1) отношение A ∩ cellFrontier (n+1) j замкнуто.
LaTeX
$$$$\forall X [t]\,[CWComplex\,C]\ [T_2Space\,X]\{A: Set\,X\}\{n:\mathbb N\}\Big(\forall m \le n, \forall j \in cell\,C\,m, IsClosed(A \cap closedCell\,m\, j)\Big) \Rightarrow \Big(\forall j \in cell\,C\,(n+1), IsClosed(A \cap D) \Rightarrow IsClosed(A \cap cellFrontier\,(n+1)\, j)\Big)$$$$
Lean4
theorem isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell [CWComplex C] [T2Space X] {A : Set X} {n : ℕ}
(hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed (A ∩ closedCell m j)) (j : cell C (n + 1)) :
IsClosed (A ∩ cellFrontier (n + 1) j) :=
RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j
(by simp only [inter_empty, isClosed_empty])
