Theorems · Definition · algebraic topology

Topology.RelCWComplex.Subcomplex.I

{X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        Topology.RelCWComplex.Subcomplex C → (n : ℕ) → Set (Topology.RelCWComplex.cell C n)

The indexing set of cells of the subcomplex.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

32 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplex