English
A subcomplex of a RelCWComplex is again a RelCWComplex.
Русский
Подкомплекс RelCWComplex снова является RelCWComplex.
LaTeX
$$RelCWComplex E D$$
Lean4
/-- A subcomplex is again a CW complex. -/
@[simps]
instance instRelCWComplex [T2Space X] [RelCWComplex C D] (E : Subcomplex C) : RelCWComplex E D
where
cell n := E.I n
map n i := map (C := C) n i
source_eq n i := source_eq (C := C) n i
continuousOn n i := continuousOn (C := C) n i
continuousOn_symm n i := continuousOn_symm (C := C) n i
pairwiseDisjoint' := by
intro ⟨n, i⟩ _ ⟨m, j⟩ _ hne
refine @pairwiseDisjoint' _ _ C D _ ⟨n, i⟩ trivial ⟨m, j⟩ trivial ?_
exact Function.injective_id.sigma_map (fun _ ↦ Subtype.val_injective) |>.ne hne
disjointBase' n i := disjointBase' (C := C) n i
mapsTo := by
intro n i
rcases cellFrontier_subset_finite_openCell (C := C) n i with ⟨J, hJ⟩
use fun m ↦ Finset.preimage (J m) Subtype.val Subtype.val_injective.injOn
rw [mapsTo_iff_image_subset]
intro x hx
specialize hJ hx
simp_rw [iUnion_coe_set, mem_union, mem_iUnion, Finset.mem_preimage, exists_prop,
Decidable.or_iff_not_imp_left] at hJ ⊢
intro h
specialize hJ h
obtain ⟨m, hmn, j, hj, hxj⟩ := hJ
suffices j ∈ E.I m from ⟨m, hmn, j, this, hj, openCell_subset_closedCell _ _ hxj⟩
have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx
by_contra hj'
exact E.disjoint_openCell_subcomplex_of_not_mem hj' |>.notMem_of_mem_left hxj this
closed' A hA
h :=
by
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell (subset_trans hA (subset_complex (C := C) E)) h.2
intro n _ j
by_cases hj : j ∈ E.I n
· exact Or.intro_right _ (h.1 n ⟨j, hj⟩)
· exact Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)
isClosedBase := isClosedBase (C := C)
union' := union_closedCell E
