English
If a RelCWComplex is finite-type, then there is a finite description of its cells and maps making it finite.
Русский
Если RelCWComplex конечного типа, то существует конечное описание клеток и отображений, задающее его.
LaTeX
$$$$ \\text{mkFiniteType}(C,D,\\dots) \\Rightarrow \\text{Finite}(C,D). $$$$
Lean4
/-- 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'`. -/
@[simps! -isSimp]
def mkFinite.{u} {X : Type u} [TopologicalSpace X] (C : Set X) (cell : (n : ℕ) → Type u)
(map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X)
(eventually_isEmpty_cell : ∀ᶠ n in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), _root_.Finite (cell n))
(source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1)
(continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (map n i) (closedBall 0 1))
(continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (map n i).symm (map n i).target)
(pairwiseDisjoint' : (univ : Set (Σ n, cell n)).PairwiseDisjoint (fun ni ↦ map ni.1 ni.2 '' ball 0 1))
(mapsTo_iff_image_subset :
∀ (n : ℕ) (i : cell n), MapsTo (map n i) (sphere 0 1) (⋃ (m < n) (j : cell m), map m j '' closedBall 0 1))
(union' : ⋃ (n : ℕ) (j : cell n), map n j '' closedBall 0 1 = C) : CWComplex C :=
(RelCWComplex.mkFinite C ∅ (cell := cell) (map := map) (eventually_isEmpty_cell := eventually_isEmpty_cell)
(finite_cell := finite_cell) (source_eq := source_eq) (continuousOn := continuousOn) (continuousOn_symm :=
continuousOn_symm) (pairwiseDisjoint' := pairwiseDisjoint') (disjointBase' := by
simp only [disjoint_empty, implies_true]) (mapsTo := by simpa only [empty_union]) (isClosedBase := isClosed_empty)
(union' := by simpa only [empty_union])).toCWComplex
