isClosed_closedCell — Mathlib

English

In a RelCWComplex placed in a T2 space, every closed cell is closed.

Русский

В пространстве Х, удовлетворяющем условию Х2, каждая замкнутая клетка замкнута.

LaTeX

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

Lean4

theorem isClosed_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (closedCell n i) :=
  isCompact_closedCell.isClosed

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