iUnion_cellFrontier_subset_skeletonLT

English

The union over all cells j at level l of their frontiers is contained in skeletonLT C l.

Русский

Объединение фронтиров клеток на уровне l содержится в skeletonLT C l.

LaTeX

$$$\\bigcup_{j\\in\\mathrm{cell}(C,l)} \\mathrm{cellFrontier}(l,j) \\subseteq \\mathrm{skeletonLT}(C,D;l)$$$

Lean4

theorem iUnion_cellFrontier_subset_skeletonLT [RelCWComplex C D] (l : ℕ) :
    ⋃ (j : cell C l), cellFrontier l j ⊆ skeletonLT C l :=
  iUnion_subset (fun _ ↦ cellFrontier_subset_skeletonLT _ _)

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