English
Let X be a topological space and C, D form a RelCWComplex. For every n and i ∈ cell C n, the frontier of i together with the open cell equals the closed cell: cellFrontier n i ∪ openCell n i = closedCell n i.
Русский
Пусть X — топологическое пространство, C и D образуют RelCWComplex. Тогда для любой размерности n и клетки i ∈ cell C n выполняется: cellFrontier n i ∪ openCell 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 \cup openCell n i = closedCell n i$$$
Lean4
theorem cellFrontier_union_openCell_eq_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
cellFrontier n i ∪ openCell n i = closedCell n i :=
by
rw [cellFrontier, openCell, closedCell, ← image_union]
congrm map n i '' ?_
exact sphere_union_ball