English
Let C D be a RelCWComplex in a T2-space X. For every n and cell j of dimension n, the interior of D is disjoint from the corresponding closed cell: interior(D) ∩ closedCell(n, j) = ∅.
Русский
Пусть C D — RelCWComplex в пространстве T2. Для каждой размерности n и клетки j размерности n, interior(D) ∩ closedCell(n, j) = ∅.
LaTeX
$$$$ \\operatorname{Disjoint}(\\operatorname{interior}(D), \\operatorname{closedCell}(n,j)). $$$$
Lean4
theorem disjoint_interior_base_closedCell [T2Space X] [RelCWComplex C D] {n : ℕ} {j : cell C n} :
Disjoint (interior D) (closedCell n j) :=
by
rw [disjoint_iff_inter_eq_empty]
by_contra h
push_neg at h
rw [← closure_openCell_eq_closedCell, inter_comm, closure_inter_open_nonempty_iff isOpen_interior] at h
rcases h with ⟨x, xmemcell, xmemD⟩
suffices x ∈ (skeletonLT C 0 : Set X) ∩ openCell n j by
rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this
exact ⟨(skeletonLT C 0).base_subset (interior_subset xmemD), xmemcell⟩
