Theorems · Inductive type · algebraic topology

Topology.RelCWComplex.Finite

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

A CW complex is finite if it is finite dimensional and of finite type.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplex