English
Let X be a topological space and C, D ⊆ X form a relative CW complex. For any subset A ⊆ X and any n ∈ ℕ, if for every m ≤ n and every cell j ∈ cell C m we have A ∩ closedCell m j closed, and A ∩ D is closed, then for every j ∈ cell C (n+1) the intersection A ∩ cellFrontier (n+1) j is closed.
Русский
Пусть X — топологическое пространство, C, D ⊆ X задают_REL CW_слой. Для любой A ⊆ X и любого n ∈ ℕ, если для каждого m ≤ n и каждой клетки j ∈ cell C m имеет место, что A ∩ closedCell m j замкнуто, и A ∩ D замкнуто, тогда для каждой j ∈ cell C (n+1)
A ∩ cellFrontier (n+1) j замкнуто.
LaTeX
$$$$\forall X [t]\,(C\,D: Set\,X)\,[RelCWComplex\,C\,D]\,[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) \to \Big(\forall j \in cell\,C\,(n+1), IsClosed(A \cap D) \Rightarrow IsClosed(A \cap cellFrontier\,(n+1)\, j)\Big)$$$$
Lean4
/-- If for all `m ≤ n` and every `i : cell C m` the intersection `A ∩ closedCell m j` is closed
and `A ∩ D` is closed then `A ∩ cellFrontier (n + 1) j` is closed for every
`j : cell C (n + 1)`. -/
theorem isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell [RelCWComplex C D] [T2Space X] {A : Set X}
{n : ℕ} (hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed (A ∩ closedCell m j)) (j : cell C (n + 1))
(hD : IsClosed (A ∩ D)) : IsClosed (A ∩ cellFrontier (n + 1) j) := by
-- this is a consequence of `cellFrontier_subset_base_union_finite_closedCell`
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (n + 1) j
rw [← inter_eq_right.2 hI, ← inter_assoc]
refine IsClosed.inter ?_ isClosed_cellFrontier
simp_rw [inter_union_distrib_left, inter_iUnion, ←
iUnion_subtype (fun m ↦ m < n + 1) (fun m ↦ ⋃ i ∈ I m, A ∩ closedCell m i)]
apply hD.union
apply isClosed_iUnion_of_finite
intro ⟨m, mlt⟩
rw [← iUnion_subtype (fun i ↦ i ∈ I m) (fun i ↦ A ∩ closedCell m i.1)]
exact isClosed_iUnion_of_finite (fun ⟨j, _⟩ ↦ hn m (Nat.le_of_lt_succ mlt) j)
