English
If n ≤ m for a RelCWComplex C D and j ∈ cell C m, then skeletonLT(C, n) and openCell(m, j) are disjoint.
Русский
Если n ≤ m для RelCWComplex C D и j ∈ cell C m, то skeletonLT(C, n) и openCell(m, j) попарно непересекаются.
LaTeX
$$$$ skeletonLT(C, n) \\cap openCell(m,j) = \\emptyset \\quad\\text{whenever } n \\le m.$$$
Lean4
/-- A skeleton and an open cell of a higher dimension are disjoint. -/
theorem disjoint_skeletonLT_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ m) :
Disjoint (skeletonLT C n : Set X) (openCell m j) := by
-- This is a consequence of `iUnion_openCell_eq_skeletonLT` and `disjoint_openCell_of_ne`
simp_rw [← iUnion_openCell_eq_skeletonLT, disjoint_union_left, disjoint_iUnion_left]
refine ⟨(disjointBase m j).symm, ?_⟩
intro l hln i
apply disjoint_openCell_of_ne
intro
simp_all only [Sigma.mk.inj_iff]
exact (lt_self_iff_false m).mp (ENat.coe_lt_coe.1 (hln.trans_le hnm))
