Structures · Topology
SigmaCompactSpace
A σ-compact space is a space that is the union of a countable collection of compact subspaces.
Note that a locally compact separable T₂ space need not be σ-compact.
The sequence can be extracted using compactCovering.
- Shape
- One type argument · adds isSigmaCompact_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- Prod
- ULift
- Sum
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by72
- compactCovering
- isCompact_compactCovering
- Module.Basis.map_addHaar
- iUnion_compactCovering
- ae_eq_zero_of_integral_contMDiff_smul_eq_zero
- exists_mem_compactCovering
- countable_cover_nhds_of_sigmaCompact
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
- SmoothPartitionOfUnity.exists_isSubordinate
- exists_contMDiffMap_zero_one_of_isClosed
- exists_contMDiff_support_eq_eq_one_iff
- Continuous.exists_contMDiff_approx_and_eqOn
- exists_contMDiffMap_forall_mem_convex_of_local
- SmoothBumpCovering.exists_isSubordinate
- ChartedSpace.secondCountable_of_sigmaCompact
- Metric.exists_contMDiffMap_forall_closedEBall_subset
- SigmaCompactSpace.exists_compact_covering
- iUnion_closure_compactCovering
- countable_cover_nhdsWithin_of_sigmaCompact
- IsOpen.exists_contMDiff_support_eq
- exists_contMDiffMap_zero_one_nhds_of_isClosed
- SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source
- ae_eq_of_integral_contMDiff_smul_eq
- IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero
- smul_singleton_mem_nhds_of_sigmaCompact
- CompactExhaustion.choice
- isOpenMap_smul_of_sigmaCompact
- SigmaCompactSpace.isSigmaCompact_univ
- isOpenMap_vadd_of_sigmaCompact
- isSigmaCompact_univ
- MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero'
- MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
- compactCovering_subset
- Topology.IsClosedEmbedding.sigmaCompactSpace
- exists_contMDiffSection_forall_mem_convex_of_local
- vadd_singleton_mem_nhds_of_sigmaCompact
- exists_contMDiffMap_forall_mem_convex_of_local_const
- isSigmaCompact_range
- Manifold.metrizableSpace
- instSigmaCompactSpaceSum
- Metric.exists_contMDiffMap_forall_closedBall_subset
- CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace
- AddMonoidHom.isOpenMap_of_sigmaCompact
- exists_contMDiff_zero_iff_one_iff_of_isClosed
- MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure
- ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace
- compactCovering.congr_simp
- MonoidHom.isOpenMap_of_sigmaCompact
- ContinuousMap.instPseudoMetrizableSpace
- MeasureTheory.SigmaFinite.of_isFiniteMeasureOnCompacts
Ancestors0
No ancestors.