Loogle!

Result

Found 199 declarations mentioning Topology.RelCWComplex.cell.

• Topology.RelCWComplex.cell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} (C : Set X) {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) : Type u
• Topology.RelCWComplex.cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Set X
• Topology.RelCWComplex.closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Set X
• Topology.RelCWComplex.openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Set X
• Topology.RelCWComplex.map 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : PartialEquiv (Fin n → ℝ) X
• Topology.RelCWComplex.Subcomplex.I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (self : Topology.RelCWComplex.Subcomplex C) (n : ℕ) : Set (Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.closedCell_nonempty 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.closedCell n j).Nonempty
• Topology.RelCWComplex.openCell_nonempty 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.openCell n j).Nonempty
• Topology.CWComplex.isCompact_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsCompact (Topology.RelCWComplex.cellFrontier n i)
• Topology.CWComplex.isCompact_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsCompact (Topology.RelCWComplex.closedCell n i)
• Topology.RelCWComplex.isCompact_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsCompact (Topology.RelCWComplex.cellFrontier n i)
• Topology.RelCWComplex.isCompact_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsCompact (Topology.RelCWComplex.closedCell n i)
• Topology.CWComplex.cell_def 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.CWComplex C] (n : ℕ) : Topology.RelCWComplex.cell C n = Topology.CWComplex.cell C n
• Topology.CWComplex.cellFrontier_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n j ⊆ C
• Topology.CWComplex.closedCell_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ C
• Topology.CWComplex.isClosed_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsClosed (Topology.RelCWComplex.cellFrontier n i)
• Topology.CWComplex.isClosed_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsClosed (Topology.RelCWComplex.closedCell n i)
• Topology.CWComplex.openCell_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ C
• Topology.RelCWComplex.cellFrontier_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n j ⊆ C
• Topology.RelCWComplex.closedCell_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ C
• Topology.RelCWComplex.isClosed_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsClosed (Topology.RelCWComplex.cellFrontier n i)
• Topology.RelCWComplex.isClosed_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {i : Topology.RelCWComplex.cell C n} : IsClosed (Topology.RelCWComplex.closedCell n i)
• Topology.RelCWComplex.openCell_subset_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ C
• Topology.CWComplex.closedCell_zero_injective 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective (Topology.RelCWComplex.closedCell 0)
• Topology.CWComplex.openCell_zero_injective 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective (Topology.RelCWComplex.openCell 0)
• Topology.RelCWComplex.closedCell_zero_injective 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective (Topology.RelCWComplex.closedCell 0)
• Topology.RelCWComplex.openCell_zero_injective 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective (Topology.RelCWComplex.openCell 0)
• Topology.RelCWComplex.toCWComplex_cell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.RelCWComplex C ∅] (n : ℕ) : Topology.CWComplex.cell C n = Topology.RelCWComplex.cell C n
• Topology.CWComplex.cellFrontier_subset_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n i ⊆ Topology.RelCWComplex.closedCell n i
• Topology.CWComplex.openCell_subset_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n i ⊆ Topology.RelCWComplex.closedCell n i
• Topology.RelCWComplex.cellFrontier_subset_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n i ⊆ Topology.RelCWComplex.closedCell n i
• Topology.RelCWComplex.openCell_subset_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n i ⊆ Topology.RelCWComplex.closedCell n i
• Topology.CWComplex.cellFrontier_zero_eq_empty 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.cellFrontier 0 j = ∅
• Topology.RelCWComplex.cellFrontier_zero_eq_empty 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.cellFrontier 0 j = ∅
• Topology.CWComplex.closure_openCell_eq_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {j : Topology.RelCWComplex.cell C n} : closure (Topology.RelCWComplex.openCell n j) = Topology.RelCWComplex.closedCell n j
• Topology.RelCWComplex.closure_openCell_eq_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {n : ℕ} {j : Topology.RelCWComplex.cell C n} : closure (Topology.RelCWComplex.openCell n j) = Topology.RelCWComplex.closedCell n j
• Topology.RelCWComplex.union 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j = C
• Topology.RelCWComplex.union_iUnion_openCell_eq_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j = C
• Topology.CWComplex.nonempty_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] {n : ℕ} (hn : n ≠ 0) (j : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.cellFrontier n j).Nonempty
• Topology.RelCWComplex.nonempty_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] {n : ℕ} (hn : n ≠ 0) (j : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.cellFrontier n j).Nonempty
• Topology.CWComplex.cellFrontier_union_openCell_eq_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n i ∪ Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.closedCell n i
• Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n i ∪ Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.closedCell n i
• Topology.RelCWComplex.toCWComplex_map 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.RelCWComplex C ∅] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.CWComplex.map n i = Topology.RelCWComplex.map n i
• Topology.RelCWComplex.openCell_congr 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) {s t✝ : Topology.RelCWComplex.cell C n} (st : Topology.RelCWComplex.openCell n s = Topology.RelCWComplex.openCell n t✝) : s = t✝
• Topology.CWComplex.injective_map_zero 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective fun x => ↑(Topology.RelCWComplex.map 0 x) ![]
• Topology.RelCWComplex.injective_map_zero 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : Function.Injective fun x => ↑(Topology.RelCWComplex.map 0 x) ![]
• Topology.CWComplex.cellFrontier_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)
• Topology.CWComplex.closedCell_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.CWComplex.openCell_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.RelCWComplex.cellFrontier_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.cellFrontier n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)
• Topology.RelCWComplex.closedCell_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.RelCWComplex.openCell_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.CWComplex.disjointBase 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Disjoint (Topology.RelCWComplex.openCell n i) D
• Topology.RelCWComplex.disjointBase 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Disjoint (Topology.RelCWComplex.openCell n i) D
• Topology.CWComplex.skeletonLT_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ∞) (l : ℕ) : (Topology.RelCWComplex.skeletonLT C n).I l = {x | ↑l < n}
• Topology.RelCWComplex.skeletonLT_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ∞) (l : ℕ) : (Topology.RelCWComplex.skeletonLT C n).I l = {x | ↑l < n}
• Topology.CWComplex.iUnion_openCell_eq_complex 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j = C
• Topology.CWComplex.map_zero_mem_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.closedCell n i
• Topology.CWComplex.map_zero_mem_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.openCell n i
• Topology.CWComplex.union 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] : ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j = C
• Topology.RelCWComplex.closed 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) ∧ IsClosed (A ∩ D)
• Topology.RelCWComplex.map_zero_mem_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.closedCell n i
• Topology.RelCWComplex.map_zero_mem_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.openCell n i
• Topology.CWComplex.closed 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] (C : Set X) [Topology.CWComplex C] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ ∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)
• Topology.CWComplex.closedCell_zero_eq_singleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.closedCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
• Topology.CWComplex.openCell_zero_eq_singleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.openCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
• Topology.RelCWComplex.closedCell_zero_eq_singleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.closedCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
• Topology.RelCWComplex.openCell_zero_eq_singleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {j : Topology.RelCWComplex.cell C 0} : Topology.RelCWComplex.openCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
• Topology.RelCWComplex.disjoint_interior_base_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ} {j : Topology.RelCWComplex.cell C n} : Disjoint (interior D) (Topology.RelCWComplex.closedCell n j)
• Topology.CWComplex.iUnion_cellFrontier_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (l : ℕ) : ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑l)
• Topology.CWComplex.iUnion_cellFrontier_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (l : ℕ) : ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑l)
• Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (l : ℕ) : ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑l)
• Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (l : ℕ) : ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑l)
• Topology.RelCWComplex.continuousOn_symm 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ContinuousOn (↑(Topology.RelCWComplex.map n i).symm) (Topology.RelCWComplex.map n i).target
• Topology.RelCWComplex.Subcomplex.copy 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I) : Topology.RelCWComplex.Subcomplex C
• Topology.CWComplex.closedCell_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.CWComplex.openCell_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.RelCWComplex.closedCell_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.RelCWComplex.openCell_subset_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : Topology.RelCWComplex.openCell n j ⊆ ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.RelCWComplex.disjoint_base_iUnion_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Disjoint D (⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j)
• Topology.RelCWComplex.source_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : (Topology.RelCWComplex.map n i).source = Metric.ball 0 1
• Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] : Disjoint (interior D) (⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n j)
• Topology.CWComplex.cellFrontier_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : Topology.RelCWComplex.cellFrontier (n + 1) j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.RelCWComplex.cellFrontier_subset_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : Topology.RelCWComplex.cellFrontier (n + 1) j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
• Topology.CWComplex.Subcomplex.copy_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I) : E.copy F hF J hJ = E
• Topology.RelCWComplex.Subcomplex.copy_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I) : E.copy F hF J hJ = E
• Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {A : Set X} (hAC : A ⊆ C) (hDA : IsClosed (A ∩ D)) (h : ∀ (n : ℕ), 0 < n → ∀ (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) : IsClosed A
• Topology.RelCWComplex.continuousOn 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ContinuousOn (↑(Topology.RelCWComplex.map n i)) (Metric.closedBall 0 1)
• Topology.CWComplex.coe_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ∞) : ↑(Topology.RelCWComplex.skeletonLT C n) = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.closedCell m j
• Topology.RelCWComplex.coe_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ∞) : ↑(Topology.RelCWComplex.skeletonLT C n) = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.closedCell m j
• Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ∞) : D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeletonLT C n)
• Topology.CWComplex.Subcomplex.coe_copy 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I) : ↑(E.copy F hF J hJ) = F
• Topology.RelCWComplex.Subcomplex.coe_copy 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I) : ↑(E.copy F hF J hJ) = F
• Topology.CWComplex.disjoint_skeletonLT_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n ≤ ↑m) : Disjoint (↑(Topology.RelCWComplex.skeletonLT C n)) (Topology.RelCWComplex.openCell m j)
• Topology.CWComplex.disjoint_skeleton_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (nlem : n < ↑m) : Disjoint (↑(Topology.RelCWComplex.skeleton C n)) (Topology.RelCWComplex.openCell m j)
• Topology.RelCWComplex.disjoint_skeletonLT_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n ≤ ↑m) : Disjoint (↑(Topology.RelCWComplex.skeletonLT C n)) (Topology.RelCWComplex.openCell m j)
• Topology.RelCWComplex.disjoint_skeleton_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (nlem : n < ↑m) : Disjoint (↑(Topology.RelCWComplex.skeleton C n)) (Topology.RelCWComplex.openCell m j)
• Topology.CWComplex.map_zero_eq_self_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {x z : Topology.RelCWComplex.cell C 0} : ↑(Topology.RelCWComplex.map 0 x) ![] = ↑(Topology.RelCWComplex.map 0 z) ![] ↔ x = z
• Topology.RelCWComplex.map_zero_eq_self_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {x z : Topology.RelCWComplex.cell C 0} : ↑(Topology.RelCWComplex.map 0 x) ![] = ↑(Topology.RelCWComplex.map 0 z) ![] ↔ x = z
• Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] [T2Space X] {A : Set X} (hAC : A ⊆ C) (h : ∀ (n : ℕ), 0 < n → ∀ (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) : IsClosed A
• Topology.RelCWComplex.union' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] : D ∪ ⋃ n, ⋃ j, ↑(Topology.RelCWComplex.map n j) '' Metric.closedBall 0 1 = C
• Topology.CWComplex.pairwiseDisjoint 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Set.univ.PairwiseDisjoint fun ni => Topology.RelCWComplex.openCell ni.fst ni.snd
• Topology.CWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n ≤ ↑m) : ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.closedCell m j = ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.cellFrontier m j
• Topology.CWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n < ↑m) : ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.closedCell m j = ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.cellFrontier m j
• Topology.RelCWComplex.pairwiseDisjoint 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Set.univ.PairwiseDisjoint fun ni => Topology.RelCWComplex.openCell ni.fst ni.snd
• Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n ≤ ↑m) : ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.closedCell m j = ↑(Topology.RelCWComplex.skeletonLT C n) ∩ Topology.RelCWComplex.cellFrontier m j
• Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : Topology.RelCWComplex.cell C m} (hnm : n < ↑m) : ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.closedCell m j = ↑(Topology.RelCWComplex.skeleton C n) ∩ Topology.RelCWComplex.cellFrontier m j
• Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {A : Set X} {n : ℕ} (hn : ∀ m ≤ n, ∀ (j : Topology.RelCWComplex.cell C m), IsClosed (A ∩ Topology.RelCWComplex.closedCell m j)) (j : Topology.RelCWComplex.cell C (n + 1)) (hD : IsClosed (A ∩ D)) : IsClosed (A ∩ Topology.RelCWComplex.cellFrontier (n + 1) j)
• Topology.RelCWComplex.mem_skeletonLT_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {x : X} : x ∈ Topology.RelCWComplex.skeletonLT C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
• Topology.RelCWComplex.mem_skeleton_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] {n : ℕ∞} {x : X} : x ∈ Topology.RelCWComplex.skeleton C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
• Topology.CWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeletonLT C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell n j = ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.RelCWComplex.closed' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (A : Set X) (hAC : A ⊆ C) : (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ ↑(Topology.RelCWComplex.map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A
• Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeletonLT C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell n j = ↑(Topology.RelCWComplex.skeletonLT C (↑n + 1))
• Topology.CWComplex.disjoint_openCell_of_ne 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n m : ℕ} {i : Topology.RelCWComplex.cell C n} {j : Topology.RelCWComplex.cell C m} (ne : ⟨n, i⟩ ≠ ⟨m, j⟩) : Disjoint (Topology.RelCWComplex.openCell n i) (Topology.RelCWComplex.openCell m j)
• Topology.RelCWComplex.disjointBase' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Disjoint (↑(Topology.RelCWComplex.map n i) '' Metric.ball 0 1) D
• Topology.RelCWComplex.disjoint_openCell_of_ne 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n m : ℕ} {i : Topology.RelCWComplex.cell C n} {j : Topology.RelCWComplex.cell C m} (ne : ⟨n, i⟩ ≠ ⟨m, j⟩) : Disjoint (Topology.RelCWComplex.openCell n i) (Topology.RelCWComplex.openCell m j)
• Topology.CWComplex.eq_of_not_disjoint_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {j : Topology.RelCWComplex.cell C n} {m : ℕ} {i : Topology.RelCWComplex.cell C m} (h : ¬Disjoint (Topology.RelCWComplex.openCell n j) (Topology.RelCWComplex.openCell m i)) : ⟨n, j⟩ = ⟨m, i⟩
• Topology.RelCWComplex.eq_of_not_disjoint_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] {n : ℕ} {j : Topology.RelCWComplex.cell C n} {m : ℕ} {i : Topology.RelCWComplex.cell C m} (h : ¬Disjoint (Topology.RelCWComplex.openCell n j) (Topology.RelCWComplex.openCell m i)) : ⟨n, j⟩ = ⟨m, i⟩
• Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [T2Space X] {A : Set X} (hAC : A ⊆ C) (hDA : IsClosed (A ∩ D)) (h : ∀ (n : ℕ), 0 < n → ∀ (j : Topology.RelCWComplex.cell C n), Disjoint A (Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) : IsClosed A
• Topology.RelCWComplex.iUnion_openCell_eq_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ∞) : D ∪ ⋃ m, ⋃ (_ : ↑m < n + 1), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeleton C n)
• Topology.RelCWComplex.Subcomplex.mk 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (carrier : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closed' : IsClosed carrier) (union' : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier) : Topology.RelCWComplex.Subcomplex C
• Topology.RelCWComplex.Subcomplex.mk'' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.RelCWComplex E D] (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : Topology.RelCWComplex.Subcomplex C
• Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] [T2Space X] {A : Set X} {n : ℕ} (hn : ∀ m ≤ n, ∀ (j : Topology.RelCWComplex.cell C m), IsClosed (A ∩ Topology.RelCWComplex.closedCell m j)) (j : Topology.RelCWComplex.cell C (n + 1)) : IsClosed (A ∩ Topology.RelCWComplex.cellFrontier (n + 1) j)
• Topology.CWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] [T2Space X] {A : Set X} (hAC : A ⊆ C) (h : ∀ (n : ℕ), 0 < n → ∀ (j : Topology.RelCWComplex.cell C n), Disjoint A (Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) : IsClosed A
• Topology.RelCWComplex.Subcomplex.union' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (self : Topology.RelCWComplex.Subcomplex C) : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = self.carrier
• Topology.CWComplex.iUnion_openCell_eq_skeletonLT 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] (n : ℕ∞) : ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeletonLT C n)
• Topology.RelCWComplex.Subcomplex.union 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ↑E
• Topology.RelCWComplex.Subcomplex.coe_mk'' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.RelCWComplex E D] (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : ↑(Topology.RelCWComplex.Subcomplex.mk'' C E I union) = E
• Topology.CWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeleton C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell (n + 1) j = ↑(Topology.RelCWComplex.skeleton C (↑n + 1))
• Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeleton C ↑n) ∪ ⋃ j, Topology.RelCWComplex.closedCell (n + 1) j = ↑(Topology.RelCWComplex.skeleton C (↑n + 1))
• Topology.RelCWComplex.Subcomplex.mk''_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.RelCWComplex E D] (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ) : (Topology.RelCWComplex.Subcomplex.mk'' C E I union).I n = I n
• Topology.CWComplex.exists_mem_openCell_of_mem_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] {n : ℕ∞} {x : X} : x ∈ Topology.RelCWComplex.skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
• Topology.CWComplex.mem_skeletonLT_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] {n : ℕ∞} {x : X} : x ∈ Topology.RelCWComplex.skeletonLT C n ↔ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
• Topology.CWComplex.mem_skeleton_iff 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] {n : ℕ∞} {x : X} : x ∈ Topology.RelCWComplex.skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
• Topology.CWComplex.iUnion_openCell_eq_skeleton 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] (n : ℕ∞) : ⋃ m, ⋃ (_ : ↑m < n + 1), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeleton C n)
• Topology.CWComplex.exists_cellFrontier_one_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) : ∃ x y, Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y
• Topology.RelCWComplex.Subcomplex.mk' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : Topology.RelCWComplex.Subcomplex C
• Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.closedCell m j
• Topology.RelCWComplex.cellFrontier_subset_finite_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.openCell m j
• Topology.CWComplex.Subcomplex.mk'' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.CWComplex E] (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : Topology.RelCWComplex.Subcomplex C
• Topology.RelCWComplex.Subcomplex.coe_mk' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : ↑(Topology.RelCWComplex.Subcomplex.mk' C E I closedCell_subset union) = E
• Topology.RelCWComplex.eq_of_eq_union_iUnion 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (I J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hIJ : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j) : I = J
• Topology.RelCWComplex.Subcomplex.mk'_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ) : (Topology.RelCWComplex.Subcomplex.mk' C E I closedCell_subset union).I n = I n
• Topology.CWComplex.cellFrontier_one_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (e : Topology.RelCWComplex.cell C 1) : Topology.RelCWComplex.cellFrontier 1 e = ↑(Topology.RelCWComplex.map 1 e) '' {-1, 1}
• Topology.RelCWComplex.cellFrontier_one_eq 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (e : Topology.RelCWComplex.cell C 1) : Topology.RelCWComplex.cellFrontier 1 e = ↑(Topology.RelCWComplex.map 1 e) '' {-1, 1}
• Topology.CWComplex.Subcomplex.coe_mk'' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.CWComplex E] (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : ↑(Topology.CWComplex.Subcomplex.mk'' C E I union) = E
• Topology.CWComplex.Subcomplex.mk''_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) [Topology.CWComplex E] (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ) : (Topology.CWComplex.Subcomplex.mk'' C E I union).I n = I n
• Topology.CWComplex.Subcomplex.union 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] {E : Topology.RelCWComplex.Subcomplex C} : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ↑E
• Topology.RelCWComplex.pairwiseDisjoint' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] : Set.univ.PairwiseDisjoint fun ni => ↑(Topology.RelCWComplex.map ni.fst ni.snd) '' Metric.ball 0 1
• Topology.RelCWComplex.mapsTo 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Set.MapsTo (↑(Topology.RelCWComplex.map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.RelCWComplex.map m j) '' Metric.closedBall 0 1)
• Topology.CWComplex.Subcomplex.mk' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : Topology.RelCWComplex.Subcomplex C
• Topology.CWComplex.cellFrontier_subset_finite_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.closedCell m j
• Topology.CWComplex.cellFrontier_subset_finite_openCell 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Topology.RelCWComplex.cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, Topology.RelCWComplex.openCell m j
• Topology.CWComplex.Subcomplex.coe_mk' 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) : ↑(Topology.CWComplex.Subcomplex.mk' C E I closedCell_subset union) = E
• Topology.CWComplex.Subcomplex.mk'_I 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [Topology.CWComplex C] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ) : (Topology.CWComplex.Subcomplex.mk' C E I closedCell_subset union).I n = I n
• Topology.CWComplex.eq_of_eq_union_iUnion 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (I J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hIJ : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j) : I = J
• Topology.CWComplex.mapsTo 📋 Mathlib.Topology.CWComplex.Classical.Basic
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (n : ℕ) (i : Topology.RelCWComplex.cell C n) : ∃ I, Set.MapsTo (↑(Topology.RelCWComplex.map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.RelCWComplex.map m j) '' Metric.closedBall 0 1)
• Topology.CWComplex.FiniteType.finite_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} {inst✝ : TopologicalSpace X} {C D : Set X} {inst✝¹ : Topology.RelCWComplex C D} [self : Topology.RelCWComplex.FiniteType C] (n : ℕ) : Finite (Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.FiniteType.finite_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} {inst✝ : TopologicalSpace X} {C D : Set X} {inst✝¹ : Topology.RelCWComplex C D} [self : Topology.RelCWComplex.FiniteType C] (n : ℕ) : Finite (Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.FiniteType.mk 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (finite_cell : ∀ (n : ℕ), Finite (Topology.RelCWComplex.cell C n)) : Topology.RelCWComplex.FiniteType C
• Topology.CWComplex.finite_cells_of_finite 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [finite : Topology.RelCWComplex.Finite C] : Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
• Topology.CWComplex.finite_of_finite_cells 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (finite : Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)) : Topology.RelCWComplex.Finite C
• Topology.RelCWComplex.finite_cells_of_finite 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] [finite : Topology.RelCWComplex.Finite C] : Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.finite_of_finite_cells 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (finite : Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)) : Topology.RelCWComplex.Finite C
• Topology.CWComplex.finite_iff_finite_cells 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Topology.RelCWComplex.Finite C ↔ Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.finite_iff_finite_cells 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u_2} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Topology.RelCWComplex.Finite C ↔ Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
• Topology.CWComplex.FiniteDimensional.eventually_isEmpty_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} {inst✝ : TopologicalSpace X} {C D : Set X} {inst✝¹ : Topology.RelCWComplex C D} [self : Topology.RelCWComplex.FiniteDimensional C] : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} {inst✝ : TopologicalSpace X} {C D : Set X} {inst✝¹ : Topology.RelCWComplex C D} [self : Topology.RelCWComplex.FiniteDimensional C] : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)
• Topology.RelCWComplex.FiniteDimensional.mk 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)) : Topology.RelCWComplex.FiniteDimensional C
• Topology.CWComplex.mkFinite_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] (C : Set X) (cell : ℕ → Type u) (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n)) (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo_iff_image_subset : ∀ (n : ℕ) (i : cell n), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) : Topology.CWComplex.cell C n = Topology.RelCWComplex.cell C n
• Topology.CWComplex.mkFinite_map 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] (C : Set X) (cell : ℕ → Type u) (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n)) (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) (mapsTo_iff_image_subset : ∀ (n : ℕ) (i : cell n), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) (i : Topology.RelCWComplex.cell C n) : Topology.CWComplex.map n i = Topology.RelCWComplex.map n i
• Topology.RelCWComplex.mkFinite_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u) (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n)) (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) (mapsTo : ∀ (n : ℕ) (i : cell n), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) : Topology.RelCWComplex.cell C n = cell n
• Topology.RelCWComplex.mkFiniteType_cell 📋 Mathlib.Topology.CWComplex.Classical.Finite
  {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u) (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n)) (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) (mapsTo : ∀ (n : ℕ) (i : cell n), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) (closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A) (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ) : Topology.RelCWComplex.cell C n = cell n
• Topology.CWComplex.OneSkeletonGraph 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.CWComplex C] : Graph (Topology.RelCWComplex.cell C 0) (Topology.RelCWComplex.cell C 1)
• Topology.CWComplex.edgeSet_OneSkeletonGraph 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.CWComplex C] : (Topology.CWComplex.OneSkeletonGraph C).edgeSet = Set.univ
• Topology.CWComplex.vertexSet_OneSkeletonGraph 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.CWComplex C] : (Topology.CWComplex.OneSkeletonGraph C).vertexSet = Set.univ
• Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff_subsingleton 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) : (∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔ (Topology.RelCWComplex.cellFrontier 1 e).Subsingleton
• Topology.CWComplex.OneSkeletonGraph.not_exists_isLoopAt_iff_nontrivial 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) : (¬∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔ (Topology.RelCWComplex.cellFrontier 1 e).Nontrivial
• Topology.CWComplex.OneSkeletonGraph_isLink 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] (C : Set X) [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) (x y : Topology.RelCWComplex.cell C 0) : (Topology.CWComplex.OneSkeletonGraph C).IsLink e x y = (Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y)
• Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) : (∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔ ∃ x, Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x
• Topology.CWComplex.OneSkeletonGraph.adj_iff 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (x y : Topology.RelCWComplex.cell C 0) : (Topology.CWComplex.OneSkeletonGraph C).Adj x y ↔ ∃ e, Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x ∪ Topology.RelCWComplex.closedCell 0 y
• Topology.CWComplex.OneSkeletonGraph.isLink_iff_pair 📋 Mathlib.Topology.CWComplex.Classical.Graph
  {X : Type u_1} [TopologicalSpace X] {C : Set X} [Topology.CWComplex C] (e : Topology.RelCWComplex.cell C 1) (x y : Topology.RelCWComplex.cell C 0) : (Topology.CWComplex.OneSkeletonGraph C).IsLink e x y ↔ Topology.RelCWComplex.cellFrontier 1 e = {↑(Topology.RelCWComplex.map 0 x) ![], ↑(Topology.RelCWComplex.map 0 y) ![]}
• Topology.RelCWComplex.Subcomplex.cell_def 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) : Topology.RelCWComplex.cell (↑E) n = ↑(E.I n)
• Topology.CWComplex.Subcomplex.cellFrontier_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.cellFrontier n i ⊆ ↑E
• Topology.CWComplex.Subcomplex.closedCell_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.closedCell n i ⊆ ↑E
• Topology.CWComplex.Subcomplex.openCell_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.openCell n i ⊆ ↑E
• Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.cellFrontier n i ⊆ ↑E
• Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.closedCell n i ⊆ ↑E
• Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (hi : i ∈ E.I n) : Topology.RelCWComplex.openCell n i ⊆ ↑E
• Topology.CWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (h : i ∉ E.I n) : Disjoint (Topology.RelCWComplex.openCell n i) ↑E
• Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n} (h : i ∉ E.I n) : Disjoint (Topology.RelCWComplex.openCell n i) ↑E
• Topology.RelCWComplex.Subcomplex.cellFrontier_eq 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)) : Topology.RelCWComplex.cellFrontier n i = Topology.RelCWComplex.cellFrontier n ↑i
• Topology.RelCWComplex.Subcomplex.closedCell_eq 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)) : Topology.RelCWComplex.closedCell n i = Topology.RelCWComplex.closedCell n ↑i
• Topology.RelCWComplex.Subcomplex.openCell_eq 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)) : Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n ↑i
• Topology.RelCWComplex.Subcomplex.map_def 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)) : Topology.RelCWComplex.map n i = Topology.RelCWComplex.map n ↑i
• Topology.RelCWComplex.Subcomplex.union_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [Topology.RelCWComplex C D] (E : Topology.RelCWComplex.Subcomplex C) : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n ↑j = ↑E
• Topology.CWComplex.Subcomplex.cell_def 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) : Topology.RelCWComplex.cell (↑E) n = ↑(E.I n)
• Topology.CWComplex.Subcomplex.union_closedCell 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] (E : Topology.RelCWComplex.Subcomplex C) : ⋃ n, ⋃ j, Topology.RelCWComplex.closedCell n ↑j = ↑E
• Topology.CWComplex.Subcomplex.map_def 📋 Mathlib.Topology.CWComplex.Classical.Subcomplex
  {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [Topology.CWComplex C] (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)) : Topology.RelCWComplex.map n i = Topology.RelCWComplex.map n ↑i

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59