Theorems · Theorem · algebraic topology

Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell

∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteDimensional C],
  ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)

For some natural number n, the type cell C m is empty for all m ≥ n.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

Topology.RelCWComplex.FiniteDimensional