English
If for every cell A ∩ openCell n j is empty or A ∩ closedCell n j is closed, then A is closed.
Русский
Если для каждой клетки A ∩ openCell n j пусто или A ∩ closedCell n j замкнуто, то A замкнуто.
LaTeX
$$$$\forall {X} [t]\, [RelCWComplex C D]\ [T_2Space X] {A: Set X} (hAC: A \subset C) (hDA: IsClosed (A \cap D)) (h: \forall n (hpos: 0 < n), \forall j: cell C n, IsClosed(A \cap openCell n j) \lor IsClosed (A \cap closedCell n j)) \Rightarrow IsClosed A$$$$
Lean4
/-- If for every cell either `A ∩ openCell n j` is empty or `A ∩ closedCell n j` is closed then
`A` is closed. -/
theorem isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell [RelCWComplex C D] [T2Space X] {A : Set X}
(hAC : A ⊆ C) (hDA : IsClosed (A ∩ D))
(h : ∀ n (_ : 0 < n), ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A :=
by
apply isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell hAC hDA
intro n hn j
rcases h n hn j with h | h
· left
rw [disjoint_iff_inter_eq_empty.1 h]
exact isClosed_empty
· exact Or.inr h
