Theorems · Definition · algebraic topology

Topology.RelCWComplex.map

{X : Type u} →
  {inst : TopologicalSpace X} →
    {C : Set X} →
      {D : outParam (Set X)} →
        [self : Topology.RelCWComplex C D] → (n : ℕ) → Topology.RelCWComplex.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

44 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

Topology.RelCWComplex