English
For a CW complex, x ∈ skeleton C n iff there exists m ≤ n and j ∈ cell C m with x ∈ openCell m j.
Русский
Для CW-комплекса x ∈ skeleton C n тогда и только тогда, когда существует m ≤ n и j ∈ cell C m с x ∈ openCell m j.
LaTeX
$$$$ x \\in skeleton(C,n) \\iff \\exists m \\le n, \\exists j \\in cell(C,m),\\; x \\in openCell(m,j). $$$$
Lean4
/-- If we want to construct a CW complex of finite type, we can add the condition `finite_cell` and
relax the condition `mapsTo`. -/
@[simps -isSimp]
def mkFiniteType.{u} {X : Type u} [TopologicalSpace X] (C : Set X) (cell : (n : ℕ) → Type u)
(map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X) (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 : ∀ (n : ℕ) (i : cell n), MapsTo (map n i) (sphere 0 1) (⋃ (m < n) (j : cell m), map m j '' closedBall 0 1))
(closed' : ∀ (A : Set X) (_ : A ⊆ C), (∀ n j, IsClosed (A ∩ map n j '' closedBall 0 1)) → IsClosed A)
(union' : ⋃ (n : ℕ) (j : cell n), map n j '' closedBall 0 1 = C) : CWComplex C
where
cell := cell
map := map
source_eq := source_eq
continuousOn := continuousOn
continuousOn_symm := continuousOn_symm
pairwiseDisjoint' := pairwiseDisjoint'
mapsTo' n
i := by
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
exact mapsTo n i
closed' := closed'
union' := union'
