mk'' — Mathlib

English

An alternative version of Subcomplex.mk: E is a CW-complex; union equals E; closedCell subset not needed.

Русский

Альтернативная версия Subcomplex.mk: E — CW-комплекс; объединение равно E; не требуется отдельное замыкание ячеек.

LaTeX

$$$$\text{mk''}\;[C]\;E\;I\;[CWComplex E]\; (union) : Subcomplex C$$$$

Lean4

/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that `E` is a CW-complex. -/
@[simps -isSimp]
def mk'' [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : Π n, Set (cell C n)) [RelCWComplex E D]
    (union : D ∪ ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = E) : Subcomplex C
    where
  carrier := E
  I := I
  closed' := isClosed
  union' := union

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