English
If a CW complex is finite, then interior(D) is disjoint from the iUnion of all closed cells.
Русский
Если CW-комплекс конечен, interior(D) не пересекается с объединением всех закрытых клеток.
LaTeX
$$$$ \\operatorname{Disjoint}(\\operatorname{interior}(D), \\bigcup_{n,j} \\operatorname{closedCell}(n,j)). $$$$
Lean4
/-- If the collection of all cells (of any dimension) of a relative CW complex `C` is finite, then
`C` is finite as a CW complex. -/
theorem finite_of_finite_cells (finite : _root_.Finite (Σ n, cell C n)) : Finite C
where
eventually_isEmpty_cell := by
simp only [Filter.eventually_atTop, ge_iff_le]
cases isEmpty_or_nonempty (Σ n, cell C n)
·
exact
⟨0, by simp_all⟩
-- We take the greatest `n` such that there is a `j : cell C n` and show that this fulfills
-- the necessary conditions.
have _ := Fintype.ofFinite (Σ n, cell C n)
classical
let A := (Finset.univ : Finset (Σ n, cell C n)).image Sigma.fst
use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
intro m _
by_contra! h'
have hmA : m ∈ A := by
simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
simp only [← exists_true_iff_nonempty] at h'
obtain ⟨j, _⟩ := h'
use ⟨m, j⟩
linarith [A.le_max' m hmA]
finite_cell _ := Finite.of_injective (Sigma.mk _) sigma_mk_injective
