openCell_subset_of_mem — Mathlib

English

If E is a Subcomplex of RelCWComplex C D and i ∈ E.I n, then openCell n i is contained in E.

Русский

Если E — подкомплекс RelCWComplex C D и i ∈ E.I n, то openCell n i ⊆ E.

LaTeX

$$$$ openCell\\,n\\,i \\subseteq E. $$$$

Lean4

theorem openCell_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n}
    (hi : i ∈ E.I n) : openCell n i ⊆ E :=
  (openCell_subset_closedCell n i).trans (closedCell_subset_of_mem E hi)

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