Theorems · Definition · algebraic topology

Topology.RelCWComplex.cellFrontier

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

The boundary of the n-cell given by the index i. Use this instead of map n i '' sphere 0 1 whenever possible.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

45 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopology.RelCWComplex