Documentation

Mathlib.Topology.CWComplex.Classical.Subcomplex

Subcomplexes #

In this file we discuss subcomplexes of CW complexes. The definition of subcomplexes is in the file Mathlib/Topology/CWComplex/Classical/Basic.lean.

Main results #

References #

source
📐 coverage
theorem Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
closedCell n i ⊆ ↑E
source
📐 coverage
theorem Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
openCell n i ⊆ ↑E
source
📐 coverage
theorem Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
cellFrontier n i ⊆ ↑E
source
📐 coverage
theorem Topology.RelCWComplex.Subcomplex.union_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) :
D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(E.I n)), closedCell n ↑j = ↑E

A subcomplex is the union of its closed cells and its base.

source
📐 coverage
theorem Topology.CWComplex.Subcomplex.union_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (E : Subcomplex C) :
⋃ (n : ℕ), ⋃ (j : ↑(E.I n)), closedCell n ↑j = ↑E

A subcomplex is the union of its closed cells.

source
📐 coverage
theorem Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) {n : ℕ} {i : cell C n} (h : i ∉ E.I n) :
Disjoint (openCell n i) ↑E
source
🔸 coverage
instance Topology.RelCWComplex.Subcomplex.instRelCWComplex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) :
RelCWComplex (↑E) D

A subcomplex is again a CW complex.

Equations
    source
    📐 coverage
    @[simp]
    theorem Topology.RelCWComplex.Subcomplex.map_def {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : ↑(E.I n)) :
    map n i = map n ↑i
    source
    📐 coverage
    @[simp]
    theorem Topology.RelCWComplex.Subcomplex.cell_def {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) :
    cell (↑E) n = ↑(E.I n)
    source
    🔸 coverage
    instance Topology.CWComplex.Subcomplex.instCWComplex {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (E : Subcomplex C) :
    CWComplex ↑E

    A subcomplex is again a CW complex.

    Equations
      source
      📐 coverage
      @[simp]
      theorem Topology.CWComplex.Subcomplex.cell_def {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (E : Subcomplex C) (n : ℕ) :
      cell (↑E) n = ↑(E.I n)
      source
      📐 coverage
      @[simp]
      theorem Topology.CWComplex.Subcomplex.map_def {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (E : Subcomplex C) (n : ℕ) (i : ↑(E.I n)) :
      map n i = map n ↑i
      source
      📐 coverage
      @[simp]
      theorem Topology.RelCWComplex.Subcomplex.openCell_eq {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : ↑(E.I n)) :
      openCell n i = openCell n ↑i
      source
      📐 coverage
      @[simp]
      theorem Topology.RelCWComplex.Subcomplex.closedCell_eq {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : ↑(E.I n)) :
      closedCell n i = closedCell n ↑i
      source
      📐 coverage
      @[simp]
      theorem Topology.RelCWComplex.Subcomplex.cellFrontier_eq {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : ↑(E.I n)) :
      cellFrontier n i = cellFrontier n ↑i
      source
      📐 coverage
      instance Topology.RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] [FiniteType C] (E : Subcomplex C) :
      FiniteType ↑E
      source
      📐 coverage
      instance Topology.RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] [FiniteDimensional C] (E : Subcomplex C) :
      FiniteDimensional ↑E
      source
      📐 coverage
      instance Topology.RelCWComplex.Subcomplex.finite_subcomplex_of_finite {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] [Finite C] (E : Subcomplex C) :
      Finite ↑E

      A subcomplex of a finite CW complex is again finite.