Theorems · Definition · algebraic topology

Topology.RelCWComplex.Subcomplex.copy

{X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        (E : Topology.RelCWComplex.Subcomplex C) →
          (F : Set X) →
            F = ↑E → (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) → J = E.I → Topology.RelCWComplex.Subcomplex C

Copy of a Subcomplex with a new carrier equal to the old one. Useful to fix definitional equalities.

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

4 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopology.RelCWComplex