Theorems · Inductive type · algebraic topology

Topology.RelCWComplex.FiniteType

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

A CW complex is of finite type if cell C n is finite for every n.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

7 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplex