Theorems · Theorem · algebraic topology

Topology.RelCWComplex.mapsTo

∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I,
    Set.MapsTo (↑(Topology.RelCWComplex.map n i)) (Metric.sphere 0 1)
      (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.RelCWComplex.map m j) '' Metric.closedBall 0 1)

The boundary of a cell is contained in the union of the base with a finite union of closed cells of a lower dimension. Use RelCWComplex.cellFrontier_subset_base_union_finite_closedCell instead.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Topology.RelCWComplex