Theorems · Theorem · algebraic topology

Topology.CWComplex.FiniteType.finite_cell

∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteType C] (n : ℕ), Finite (Topology.RelCWComplex.cell C n)

Alias of Topology.RelCWComplex.FiniteType.finite_cell. cell C n is finite for every n.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Topology.RelCWComplex.FiniteType