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
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
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem.

source
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
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem.

source
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
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem.

source
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
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
theorem Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem {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
theorem Topology.CWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem {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

Alias of Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem.

source
@[deprecated Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem (since := "2026-09-28")]
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

Alias of Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem.

source
@[instance_reducible]
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
  • One or more equations did not get rendered due to their size.
source
@[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
@[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
@[instance_reducible]
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
@[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
@[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
@[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
@[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
@[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
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
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType.

source
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
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional.

source
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.

source
theorem Topology.CWComplex.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

Alias of Topology.RelCWComplex.Subcomplex.finite_subcomplex_of_finite.

A subcomplex of a finite CW complex is again finite.