Mathlib Map

Structures · Topology

Topology.RelCWComplex.FiniteDimensional

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
Shape
One type argument · adds eventually_isEmpty_cell

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by6

Ancestors0

No ancestors.