disjoint_interior_base_iUnion_closedCell

English

Let C D be a RelCWComplex in a T2-space X. Then interior(D) is disjoint from the iUnion over all n and all cells j of the closed cells: interior(D) ∩ ⋃_{n, j} closedCell(n, j) = ∅.

Русский

Пусть C D — RelCWComplex в T2-пространстве. interior(D) не пересекается с объединением всех closedCell.

LaTeX

$$$$ \\operatorname{Disjoint}(\\operatorname{interior}(D), \\bigcup_{n\\in\\mathbb{N}}\\bigcup_{j\\in cell(C,n)} \\operatorname{closedCell}(n,j)). $$$$

Lean4

theorem disjoint_interior_base_iUnion_closedCell [T2Space X] [RelCWComplex C D] :
    Disjoint (interior D) (⋃ (n : ℕ) (j : cell C n), closedCell n j) := by
  simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq, iUnion_empty]

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