Theorems · Theorem · algebraic topology

Topology.CWComplex.finite_of_finiteDimensional_finiteType

∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) {D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteType C], Topology.RelCWComplex.Finite C

Alias of Topology.RelCWComplex.finite_of_finiteDimensional_finiteType.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplexTopology.RelCWComplex.FiniteDimensionalTopology.RelCWComplex.FiniteType