mk'' — Mathlib

English

An alternative version of Subcomplex.mk'': E is CW-complex; union equals E.

Русский

Альтернативная версия 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) [h : CWComplex C] (E : Set X) (I : Π n, Set (cell C n)) [CWComplex E]
    (union : ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = E) : Subcomplex C
    where
  carrier := E
  I := I
  closed' := RelCWComplex.isClosed
  union' := by
    rw [empty_union]
    exact union

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