closure_openCell_eq_closedCell — Mathlib

English

In a RelCWComplex with T2, closure of an open cell equals the corresponding closed cell: closure(openCell n j) = closedCell n j.

Русский

В RelCWComplex с T2 пространство замыкание открытой клетки равно соответствующей замкнутой клетке: closure(openCell n j) = closedCell n j.

LaTeX

$$$\mathrm{closure}(openCell n j) = closedCell n j$$$

Lean4

theorem closure_openCell_eq_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ} {j : cell C n} :
    closure (openCell n j) = closedCell n j :=
  by
  apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n j))
  rw [closedCell, ← closure_ball 0 (by exact one_ne_zero)]
  apply ContinuousOn.image_closure
  rw [closure_ball 0 (by exact one_ne_zero)]
  exact continuousOn n j

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