Theorems · Theorem · algebraic topology

Topology.RelCWComplex.closed

∀ {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X],
  ∀ A ⊆ C,
    IsClosed A ↔
      (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) ∧
        IsClosed (A ∩ D)

Defined in

Mathlib.Topology.CWComplex.Classical.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopology.RelCWComplexT2Space