disjoint_openCell_subcomplex_of_not_mem

English

If i is a cell of C of dimension n and i ∉ E.I(n), then openCell n i is disjoint from E.

Русский

Если клетка i размерности n принадлежит C и i ∉ E.I(n), то openCell n i дисjoint с E.

LaTeX

$$Disjoint (openCell n i) E$$

Lean4

theorem disjoint_openCell_subcomplex_of_not_mem [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n}
    (h : i ∉ E.I n) : Disjoint (openCell n i) E :=
  by
  simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]
  exact ⟨disjointBase n i, fun _ _ ↦ disjoint_openCell_of_ne (by aesop)⟩

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