disjoint_openCell_of_ne — Mathlib

English

There exists a finite collection of cells such that cellFrontier is contained in their corresponding closedCells together with D.

Русский

Существует конечная коллекция клеток, так что cellFrontier ⊆ D ∪ ⋃ ClosedCells.

LaTeX

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

Lean4

theorem disjoint_openCell_of_ne [RelCWComplex C D] {n m : ℕ} {i : cell C n} {j : cell C m}
    (ne : (⟨n, i⟩ : Σ n, cell C n) ≠ ⟨m, j⟩) : Disjoint (openCell n i) (openCell m j) :=
  pairwiseDisjoint (mem_univ _) (mem_univ _) ne

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