disjoint_skeleton_openCell — Mathlib

English

If n < m for a RelCWComplex C D and j ∈ cell C m, then skeleton(C, n) and openCell(m, j) are disjoint.

Русский

Если n < m для RelCWComplex C D и j ∈ cell C m, то skeleton(C, n) и openCell(m, j) не пересекаются.

LaTeX

$$$$ skeleton(C, n) \\cap openCell(m,j) = \\emptyset \\quad\\text{whenever } n < m.$$$$

Lean4

/-- A skeleton and an open cell of a higher dimension are disjoint. -/
theorem disjoint_skeleton_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (nlem : n < m) :
    Disjoint (skeleton C n : Set X) (openCell m j) :=
  disjoint_skeletonLT_openCell (Order.add_one_le_of_lt nlem)

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