Theorems · Theorem · algebraic topology

Topology.CWComplex.continuousOn_symm

∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C] (n : ℕ)
  (i : Topology.CWComplex.cell C n),
  ContinuousOn (↑(Topology.CWComplex.map n i).symm) (Topology.CWComplex.map n i).target

The inverse of the restriction to ball 0 1 is continuous on the image.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Topology.CWComplex