RelativeCWComplex — Mathlib

English

The relative CW complex structure on C by ∅ coincides with the CW complex structure produced by toCWComplex.

Русский

Относительная CW-структура на C с основанием ∅ совпадает с CW-структурой, полученной через toCWComplex.

LaTeX

$$$(toCWComplex)(C).instRelCWComplex = h$$$

Lean4

/-- A relative CW-complex is a morphism `f : X ⟶ Y` equipped with data expressing
that `Y` identifies to the colimit of a functor `F : ℕ ⥤ TopCat` with that
`F.obj 0 ≅ X` and for any `n : ℕ`, `F.obj (n + 1)` is obtained from `F.obj n`
by attaching `n`-disks. -/
abbrev RelativeCWComplex {X Y : TopCat.{u}} (f : X ⟶ Y) :=
  RelativeCellComplex.{u} basicCell f

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