English
Interior(D) is disjoint from the union of all closed cells in a RelCWComplex.
Русский
Interior(D) не пересекается с объединением всех закрытых клеток в RelCWComplex.
LaTeX
$$$$ \\operatorname{Disjoint}(\\operatorname{interior}(D), \\bigcup_{n,j} \\operatorname{closedCell}(n,j)). $$$$
Lean4
/-- If we want to construct a finite relative CW complex we can add the conditions
`eventually_isEmpty_cell` and `finite_cell`, relax the condition `mapsTo` and remove the condition
`closed'`. -/
@[simps -isSimp]
def mkFinite.{u} {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : (n : ℕ) → Type u)
(map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X)
(eventually_isEmpty_cell : ∀ᶠ n in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), _root_.Finite (cell n))
(source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1)
(continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (map n i) (closedBall 0 1))
(continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (map n i).symm (map n i).target)
(pairwiseDisjoint' : (univ : Set (Σ n, cell n)).PairwiseDisjoint (fun ni ↦ map ni.1 ni.2 '' ball 0 1))
(disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (map n i '' ball 0 1) D)
(mapsTo :
∀ (n : ℕ) (i : cell n), MapsTo (map n i) (sphere 0 1) (D ∪ ⋃ (m < n) (j : cell m), map m j '' closedBall 0 1))
(isClosedBase : IsClosed D) (union' : D ∪ ⋃ (n : ℕ) (j : cell n), map n j '' closedBall 0 1 = C) : RelCWComplex C D
where
cell := cell
map := map
source_eq := source_eq
continuousOn := continuousOn
continuousOn_symm := continuousOn_symm
pairwiseDisjoint' := pairwiseDisjoint'
disjointBase' := disjointBase'
mapsTo n
i := by
use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
exact mapsTo n i
closed' A
asubc := by
intro h
rw [← inter_eq_left.2 asubc]
simp_rw [Filter.eventually_atTop, ge_iff_le] at eventually_isEmpty_cell
obtain ⟨N, hN⟩ := eventually_isEmpty_cell
suffices IsClosed (A ∩ (D ∪ ⋃ (n : { n : ℕ // n < N }), ⋃ j, ↑(map n j) '' closedBall 0 1))
by
convert this using 2
rw [← union', iUnion_subtype]
congrm D ∪ ⋃ n, ?_
refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))
apply iUnion_subset
intro i
have : n < N := Decidable.byContradiction fun h ↦ (hN n (Nat.ge_of_not_lt h)).false i
exact subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i
simp_rw [inter_union_distrib_left, inter_iUnion]
exact h.2.union (isClosed_iUnion_of_finite (fun n ↦ isClosed_iUnion_of_finite (h.1 n.1)))
isClosedBase := isClosedBase
union' := union'
