Theorems · Theorem · algebraic topology

Topology.CWComplex.source_eq

∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n), (Topology.CWComplex.map n i).source = Metric.ball 0 1

The source of every characteristic map of dimension n is (ball 0 1 : Set (Fin n → ℝ)).

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Topology.CWComplex