English
An alternative construction of a Subcomplex C from a carrier E, cell index I, and a union relation, requiring closedCell ⊆ E and that the union of D with open cells equals E, yields a Subcomplex.
Русский
Альтернативная конструкция Subcomplex C из носителя E, индексов клеток I и отношения объединения, требующая, чтобы closedCell ⊆ E и что объединение D с открытыми клетками равно E, образует Subcomplex.
LaTeX
$$$$\text{mk'}\;[C]\;E\;I\;(closedCell\_subset)\; (union) : Subcomplex C$$$$
Lean4
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that for every cell of the subcomplex the corresponding closed cell is a subset of `E`. -/
@[simps -isSimp]
def mk' [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : Π n, Set (cell C n))
(closedCell_subset : ∀ (n : ℕ) (i : I n), closedCell (C := C) n i ⊆ E)
(union : D ∪ ⋃ (n : ℕ) (j : I n), openCell (C := C) n j = E) : Subcomplex C
where
carrier := E
I := I
closed' :=
by
have hEC : (E : Set X) ⊆ C :=
by
simp_rw [← union, ← union_iUnion_openCell_eq_complex (C := C)]
exact union_subset_union_right D (iUnion_mono fun n ↦ iUnion_subset fun i ↦ subset_iUnion _ (i : cell C n))
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell hEC
· have : D ⊆ E := by
rw [← union]
exact subset_union_left
rw [inter_eq_right.2 this]
exact isClosedBase C
intro n _ j
by_cases h : j ∈ I n
· right
suffices closedCell n j ⊆ E by
rw [inter_eq_right.2 this]
exact isClosed_closedCell
exact closedCell_subset n ⟨j, h⟩
· left
simp_rw [← union, disjoint_union_left, disjoint_iUnion_left]
exact ⟨disjointBase n j |>.symm, fun _ _ ↦ disjoint_openCell_of_ne (by aesop)⟩
union' := union
