union_iUnion_openCell_eq_complex — Mathlib

English

D together with all open cells covers the CW complex: D ∪ ⋃_{n, j} openCell n j = C.

Русский

D вместе со всеми открытыми клетками покрывает CW-комплекс: D ∪ ⋃_{n, j} openCell n j = C.

LaTeX

$$$D \cup \bigcup_{n} \bigcup_{j} openCell (C := C) n j = C$$$

Lean4

theorem union_iUnion_openCell_eq_complex [RelCWComplex C D] : D ∪ ⋃ (n : ℕ) (j : cell C n), openCell n j = C :=
  by
  suffices D ∪ ⋃ n, ⋃ (j : cell C n), openCell n j = D ∪ ⋃ (m : ℕ) (_ : m < (⊤ : ℕ∞)) (j : cell C m), closedCell m j by
    simpa [union] using this
  simp_rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.coe_lt_top, iUnion_true]

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