isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell

English

If for every cell either A ∩ openCell n j or A ∩ closedCell n j is closed, then A is closed.

Русский

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

LaTeX

$$$$\forall {X} [t]\, [CWComplex C]\ [T_2Space X] {A: Set X} (hAC: A \subset C) (h: \forall n (\_ : 0 < n), \forall j: cell C n, IsClosed (A \cap openCell n j) \lor IsClosed (A \cap closedCell n j)) : IsClosed A$$$$

Lean4

/-- If for every cell either `A ∩ openCell n j` or `A ∩ closedCell n j` is closed then
`A` is closed. -/
theorem isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell [CWComplex C] [T2Space X] {A : Set X}
    (hAC : A ⊆ C) (h : ∀ n (_ : 0 < n), ∀ (j : cell C n), IsClosed (A ∩ openCell n j) ∨ IsClosed (A ∩ closedCell n j)) :
    IsClosed A :=
  RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell hAC (by simp) h

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