iUnion_cellFrontier_subset_skeleton

English

For each l, the union of all cellFrontier l j is contained in skeleton C l.

Русский

Для каждого l объединение cellFrontier l j ⊆ skeleton C l.

LaTeX

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

Lean4

theorem iUnion_cellFrontier_subset_skeleton [RelCWComplex C D] (l : ℕ) :
    ⋃ (j : cell C l), cellFrontier l j ⊆ skeleton C l :=
  (iUnion_cellFrontier_subset_skeletonLT l).trans (skeletonLT_mono le_self_add)

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