isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell

English

If for every n>0 and every j, either A ∩ openCell n j is empty or A ∩ closedCell n j is closed, then A is closed.

Русский

Если для каждого n>0 и каждой клетки j либо пересечение A с openCell пусто, либо A ∩ closedCell замкнуто, то A замкнуто.

LaTeX

$$$$\forall {X} [t]\,[CWComplex C]\ [T_2Space X] {A: Set X} (hAC: A \subset C) (hDA: IsClosed (A \cap D)) (h: \forall n(>0), \forall j: cell C n, Disjoint A (openCell n j) \lor IsClosed(A \cap closedCell n j)) : 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 [CWComplex C] [T2Space X] {A : Set X} (hAC : A ⊆ C)
    (h : ∀ n (_ : 0 < n), ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A :=
  RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell hAC (by simp) h

Похожие утверждения