English
Let (C, D) define a relative CW complex. Then the ambient set C is the union of all its skeleta, i.e. C = ⋃_{n∈ℕ} skeleton(C, n); equivalently, every point of C lies in some finite skeleton.
Русский
Пусть (C, D) задаёт относительный CW-комплекс. Тогда пространство C является объединением всех своих скелетов: C = ⋃_{n∈ℕ} skeleton(C, n); то есть любая точка из C принадлежит некоторому конечному скелету.
LaTeX
$$$$\\bigcup_{n \\in \\mathbb{N}} \\mathrm{skeleton}(C, n) = C.$$$$
Lean4
theorem iUnion_skeleton_eq_complex [RelCWComplex C D] : ⋃ (n : ℕ), skeleton C n = C :=
by
apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)
simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
exact
⟨subset_iUnion_of_subset 0 (skeleton C 0).base_subset, fun n i ↦
subset_iUnion_of_subset _ (openCell_subset_skeleton n i)⟩
