closedCell_subset_of_mem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem closedCell_subset_of_mem [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n}
    (hi : i ∈ E.I n) : closedCell n i ⊆ E :=
  by
  rw [← closure_openCell_eq_closedCell, E.closed.closure_subset_iff, ← E.union]
  apply subset_union_of_subset_right
  exact subset_iUnion_of_subset n (subset_iUnion (fun (j : ↑(E.I n)) ↦ openCell (C := C) n j) ⟨i, hi⟩)

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