Theorems · Definition · algebraic topology

Topology.RelCWComplex.Finite.casesOn

{X : Type u_1} →
  [inst : TopologicalSpace X] →
    {C D : Set X} →
      [inst_1 : Topology.RelCWComplex C D] →
        {motive : Topology.RelCWComplex.Finite C → Sort u} →
          (t : Topology.RelCWComplex.Finite C) →
            ([toFiniteDimensional : Topology.RelCWComplex.FiniteDimensional C] →
                [toFiniteType : Topology.RelCWComplex.FiniteType C] → motive ⋯) →
              motive t

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopology.RelCWComplex