Structures · Topology
Topology.CWComplex
Characterizing when a subspace C of a topological space X is a CW complex. Note that this
requires C to be closed. If C is not closed choose X to be C.
- Shape
- One type argument · adds cell, map, source_eq, continuousOn, continuousOn_symm, pairwiseDisjoint', mapsTo', closed', union'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by51
- Topology.CWComplex.cell
- Topology.CWComplex.map
- Topology.CWComplex.OneSkeletonGraph
- Topology.CWComplex.Subcomplex.mk''
- Topology.CWComplex.Subcomplex.mk'
- Topology.CWComplex.OneSkeletonGraph_isLink
- Topology.CWComplex.mem_skeleton_iff
- Topology.RelCWComplex.nonempty_cellFrontier
- Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff_subsingleton
- Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff
- Topology.CWComplex.cellFrontier_subset_finite_closedCell
- Topology.CWComplex.exists_cellFrontier_one_eq
- Topology.CWComplex.iUnion_openCell_eq_skeletonLT
- Topology.CWComplex.source_eq
- Topology.CWComplex.skeletonLT_zero_eq_empty
- Topology.CWComplex.Subcomplex.instCWComplex
- Topology.CWComplex.continuousOn
- Topology.CWComplex.union'
- Topology.CWComplex.mapsTo'
- Topology.CWComplex.vertexSet_OneSkeletonGraph
- Topology.CWComplex.iUnion_openCell_eq_complex
- Topology.CWComplex.Subcomplex.cell_def
- Topology.CWComplex.Subcomplex.map_def
- Topology.CWComplex.OneSkeletonGraph.not_exists_isLoopAt_iff_nontrivial
- Topology.CWComplex.nonempty_cellFrontier
- Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell
- Topology.CWComplex.union
- Topology.CWComplex.OneSkeletonGraph.adj_iff
- Topology.CWComplex.cell_def
- Topology.CWComplex.continuousOn_symm
- Topology.CWComplex.Subcomplex.union
- Topology.CWComplex.edgeSet_OneSkeletonGraph
- Topology.CWComplex.iUnion_openCell_eq_skeleton
- Topology.CWComplex.mem_skeletonLT_iff
- Topology.CWComplex.closed
- Topology.CWComplex.Subcomplex.mk'_I
- Topology.CWComplex.pairwiseDisjoint'
- Topology.CWComplex.map_def
- Topology.CWComplex.Subcomplex.coe_mk''
- Topology.CWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
- Topology.CWComplex.instRelCWComplex
- Topology.CWComplex.Subcomplex.coe_mk'
- Topology.CWComplex.OneSkeletonGraph.isLink_iff_pair
- Topology.CWComplex.mapsTo
- Topology.CWComplex.exists_mem_openCell_of_mem_skeleton
- Topology.CWComplex.closed'
- Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell
- Topology.CWComplex.Subcomplex.union_closedCell
- Topology.CWComplex.eq_of_eq_union_iUnion
- Topology.CWComplex.Subcomplex.mk''_I
Ancestors0
No ancestors.