cellFrontier_subset_of_mem — Mathlib

English

Let C, D be ambient sets with a RelCWComplex structure. Let E be a Subcomplex of C. If i is a n-dimensional cell in E (i ∈ E.I(n)), then the frontier of i is contained in E; i.e., cellFrontier(n,i) ⊆ E.

Русский

Пусть C и D образуют RelCWComplex. Пусть E — подкомплекс C. Если i принадлежит E.I(n), то граница клетки i лежит в E; то есть cellFrontier(n,i) ⊆ E.

LaTeX

$$$\forall E : Subcomplex C\,\forall n : \mathbb{N}\,\forall i : cell\ C\ n,\ (i \in E.I\ n) \Rightarrow cellFrontier\ n\ i \subseteq E$$$

Lean4

theorem cellFrontier_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n}
    (hi : i ∈ E.I n) : cellFrontier n i ⊆ E :=
  (cellFrontier_subset_closedCell n i).trans (closedCell_subset_of_mem E hi)

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