English
The instance RelCWComplex on C is defined with fields inherited from CWComplex and maps to the empty base.
Русский
Экземпляр RelCWComplex на C определяется полями, наследованными от CWComplex, с основанием пустого множества.
LaTeX
$$$RelCWComplex\;instRelCWComplex\; (C)\; D$$$
Lean4
@[simps -isSimp]
instance (priority := high) instRelCWComplex {X : Type*} [TopologicalSpace X] (C : Set X) [CWComplex C] :
RelCWComplex C ∅ where
cell := CWComplex.cell C
map := CWComplex.map
source_eq := CWComplex.source_eq
continuousOn := CWComplex.continuousOn
continuousOn_symm := CWComplex.continuousOn_symm
pairwiseDisjoint' := CWComplex.pairwiseDisjoint'
disjointBase' := by simp [disjoint_empty]
mapsTo := by simpa only [empty_union] using CWComplex.mapsTo'
closed' := by simpa only [inter_empty, isClosed_empty, and_true] using CWComplex.closed'
isClosedBase := isClosed_empty
union' := by simpa only [empty_union] using CWComplex.union'
