Theorems · Definition · algebraic topology

Topology.RelCWComplex.skeletonLT

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

A non-standard definition of the n-skeleton of a CW complex for n ∈ ℕ ∪ {∞}. This allows the base case of induction to be about the base instead of being about the union of the base and some points. The standard skeleton is defined in terms of skeletonLT. skeletonLT is preferred in statements. You should then derive the statement about skeleton.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

34 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceTopology.RelCWComplex