Theorems · Inductive type · algebraic topology

Topology.RelCWComplex.FiniteDimensional

{X : Type u} → [inst : TopologicalSpace X] → (C : Set X) → {D : Set X} → [Topology.RelCWComplex C D] → Prop

A CW complex is finite dimensional if cell C n is empty for all but finitely many n.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

5 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplex