skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

English

Version of the previous with skeleton (not LT): for n ≤ m, skeleton(C, n) ∩ closedCell(m, j) = skeleton(C, n) ∩ cellFrontier(m, j).

Русский

Версия для скелета (не LT): при n ≤ m имеем skeleton(C, n) ∩ closedCell(m, j) = skeleton(C, n) ∩ cellFrontier(m, j).

LaTeX

$$$$ (skeleton\\,C\\,n) \\cap \\text{closedCell}(m,j) = (skeleton\\,C\\,n) \\cap \\text{cellFrontier}(m,j) $$$$

Lean4

/-- Version of `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` using `skeleton`. -/
theorem skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m}
    (hnm : n < m) : (skeleton C n : Set X) ∩ closedCell m j = (skeleton C n : Set X) ∩ cellFrontier m j :=
  skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier (Order.add_one_le_of_lt hnm)

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