cellFrontier_subset_closedCell — Mathlib

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

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