Theorems · Theorem · algebraic topology

Topology.CWComplex.finiteType_mkFiniteType

∀ {X : Type u} [inst : TopologicalSpace X] (C : 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)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ 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)
  (union' : ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C), Topology.RelCWComplex.FiniteType C

A CW complex that was constructed using CWComplex.mkFiniteType is of finite type.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace