toCWComplex — Mathlib

English

The toCWComplex construction yields a CWComplex from a RelCWComplex with empty base.

Русский

Конструкция toCWComplex даёт CWComplex из RelCWComplex с пустым основанием.

LaTeX

$$$toCWComplex\; C : CWComplex\; C$$$

Lean4

/-- A relative CW complex with an empty base is an absolute CW complex. -/
@[simps -isSimp]
def toCWComplex {X : Type*} [TopologicalSpace X] (C : Set X) [RelCWComplex C ∅] : CWComplex C
    where
  cell := cell C
  map := map
  source_eq := source_eq
  continuousOn := continuousOn
  continuousOn_symm := continuousOn_symm
  pairwiseDisjoint' := pairwiseDisjoint'
  mapsTo' := by simpa using mapsTo (C := C)
  closed' := by simpa using closed' (C := C)
  union' := by simpa using union' (C := C)

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