English
Let X be a topological space and C, D subsets of X forming a RelCWComplex. Then for every n ∈ N and every i ∈ cell C n, the frontier of the cell satisfies cellFrontier n i ⊆ closedCell n i.
Русский
Пусть X — топологическое пространство, а C, D — подмножества X, образующие RelCWComplex. Тогда для любой n ∈ ℕ и любой элемент i клетки C n выполняется cellFrontier n i ⊆ closedCell n i.
LaTeX
$$$\forall {X} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : \mathbb{N}) (i : cell C n),\quad cellFrontier n i \subseteq closedCell n i$$$
Lean4
theorem cellFrontier_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ⊆ closedCell n i :=
image_mono Metric.sphere_subset_closedBall