isClosed_cellFrontier — Mathlib

English

In a RelCWComplex with T2, the frontier of a cell is closed.

Русский

В RelCWComplex с T2 пространство граница клетки замкнута.

LaTeX

$$$\forall {X} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : \mathbb{N}} {i : cell C n}, IsClosed (cellFrontier n i)$$

Lean4

theorem isClosed_cellFrontier [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (cellFrontier n i) :=
  isCompact_cellFrontier.isClosed

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