Theorems · Theorem · algebraic topology

Topology.CWComplex.injective_map_zero

∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective fun x => ↑(Topology.RelCWComplex.map 0 x) ![]

Alias of Topology.RelCWComplex.injective_map_zero. If two 0-cells have the same characteristic image point, they are equal.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopology.RelCWComplex