Theorems · Definition · algebraic topology

Topology.RelCWComplex.skeleton

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

The n-skeleton of a CW complex, for n ∈ ℕ ∪ {∞}. For statements use skeletonLT instead and then derive the statement about skeleton.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

28 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT2SpaceTopology.RelCWComplex