Theorems · Definition · algebraic topology

Topology.CWComplex.map

{X : Type u} →
  {inst : TopologicalSpace X} →
    {C : Set X} → [self : Topology.CWComplex C] → (n : ℕ) → Topology.CWComplex.cell C n → PartialEquiv (Fin n → ℝ) X

The characteristic map of the n-cell given by the index i. This map is a bijection when restricting to ball 0 1, where we consider (Fin n → ℝ) endowed with the maximum metric.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

12 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

Topology.CWComplex