English
For a RelCWComplex C D and a fixed n and i, there exists a finite family I such that the boundary of the cell i is contained in the union of D with finitely many open cells of lower dimension.
Русский
Для RelCWComplex C D и фиксированных n и i существует конечная семья I такая, что граница клетки i ограничена объединением D и конечным числом открытых клеток меньшей размерности.
LaTeX
$$$$\exists I: \Pi m, Finset (cell C m), cellFrontier n i \subseteq D \cup \bigcup_{m < n} \bigcup_{j \in I m} openCell m j$$$$
Lean4
/-- A version of `cellFrontier_subset_base_union_finite_closedCell` using open cells:
The boundary of a cell is contained in a finite union of open cells of a lower dimension. -/
theorem cellFrontier_subset_finite_openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
∃ I : Π m, Finset (cell C m), cellFrontier n i ⊆ D ∪ (⋃ (m < n) (j ∈ I m), openCell m j) := by
induction n using Nat.case_strong_induction_on with
| hz => simp [cellFrontier_zero_eq_empty]
| hi n hn =>
-- We apply `cellFrontier_subset_base_union_finite_closedCell` once and then apply
-- the induction hypothesis to the finitely many cells that
-- `cellFrontier_subset_base_union_finite_closedCell` gives us.
classical
obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i
choose p hp using hn
let I m :=
J m ∪ ((Finset.range n.succ).biUnion (fun l ↦ (J l).biUnion (fun y ↦ if h : l ≤ n then p l h y m else ∅)))
use I
intro x hx
specialize hJ hx
simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢
rcases hJ with hJ | hJ
· exact .inl hJ
obtain ⟨l, hln, j, hj, hxj⟩ := hJ
rw [← cellFrontier_union_openCell_eq_closedCell] at hxj
rcases hxj with hxj | hxj
· specialize hp l (Nat.le_of_lt_succ hln) j hxj
simp_rw [mem_union, mem_iUnion, exists_prop] at hp
refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩
· right
use l, hln, j
simp only [Nat.succ_eq_add_one, Finset.mem_union, I]
exact ⟨Or.intro_left _ hj, hxj⟩
