cellFrontier_union_openCell_eq_closedCell

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

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