English
For RelCWComplex C D, if n ≤ m, then skeleton (C, n) and openCell(m, j) are disjoint.
Русский
Для RelCWComplex C D, если n ≤ m, то skeleton(C, n) и openCell(m, j) попарно непересекаются.
LaTeX
$$$$ skeleton(C, n) \\cap openCell(m,j) = \\emptyset \\quad (n \\le m). $$$$
Lean4
/-- A CW complex that was constructed using `RelCWComplex.mkFiniteType` is of finite type. -/
theorem finiteType_mkFiniteType.{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)
(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))
(closed' :
∀ (A : Set X) (_ : A ⊆ C), ((∀ n j, IsClosed (A ∩ map n j '' closedBall 0 1)) ∧ IsClosed (A ∩ D)) → IsClosed A)
(isClosedBase : IsClosed D) (union' : D ∪ ⋃ (n : ℕ) (j : cell n), map n j '' closedBall 0 1 = C) :
letI :=
mkFiniteType C D cell map finite_cell source_eq continuousOn continuousOn_symm pairwiseDisjoint' disjointBase'
mapsTo closed' isClosedBase union'
FiniteType C :=
letI :=
mkFiniteType C D cell map finite_cell source_eq continuousOn continuousOn_symm pairwiseDisjoint' disjointBase'
mapsTo closed' isClosedBase union'
{ finite_cell := finite_cell }
