cellFrontier_subset_finite_openCell

English

Same as above but in the RelCWComplex setting; there exists a finite I with the frontier contained in D ∪ unions of open cells.

Русский

То же самое в контексте RelCWComplex; существует конечная I такая, что граница ограничена объединениями открытых клеток.

LaTeX

$$$$\exists I: \Pi m, Finset (cell C m), cellFrontier n i \subseteq D \cup \bigcup_{m < n} \bigcup_{j \in I m} openCell m j$$$$

Lean4

/-- A version of `cellFrontier_subset_finite_closedCell` using open cells: The boundary of a cell is
contained in a finite union of open cells of a lower dimension. -/
theorem cellFrontier_subset_finite_openCell [CWComplex C] (n : ℕ) (i : cell C n) :
    ∃ I : Π m, Finset (cell C m), cellFrontier n i ⊆ ⋃ (m < n) (j ∈ I m), openCell m j := by
  simpa using RelCWComplex.cellFrontier_subset_finite_openCell n i

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