Theorems · Definition · algebraic topology

Topology.CWComplex.mkFinite

{X : Type u} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      (cell : ℕ → Type u) →
        (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
          (∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) →
            (∀ (n : ℕ), Finite (cell n)) →
              (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
                (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                  (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                    (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                      (∀ (n : ℕ) (i : cell n),
                          Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                            (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) →
                        ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.CWComplex C

If we want to construct a finite CW complex we can add the conditions eventually_isEmpty_cell and finite_cell, relax the condition mapsTo and remove the condition closed'.

Defined in

Mathlib.Topology.CWComplex.Classical.Finite

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace