isCompact_closedCell — Mathlib

English

In a RelCWComplex, every closed cell is compact.

Русский

В RelCWComplex каждая замкнутая клетка компактна.

LaTeX

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

Lean4

theorem isCompact_closedCell [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (closedCell n i) :=
  (isCompact_closedBall _ _).image_of_continuousOn (continuousOn n i)

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