Structures · Topology
NoncompactSpace
X is a noncompact topological space if it is not a compact space.
- Defined in
- Mathlib.Topology.Defs.Filter
- Shape
- One type argument · adds noncompact_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances12
- Int
- Nat
- Real
- Rat
- PNat
- TopologicalSpace.NonemptyCompacts
- TopologicalSpace.Compacts
- TopologicalSpace.Closeds
- UpperHalfPlane
- Prod
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- IsCompact.ne_univ
- MeasureTheory.measure_univ_of_isAddLeftInvariant
- MeasureTheory.measure_univ_of_isMulLeftInvariant
- Metric.ediam_univ_of_noncompact
- noncompact_univ
- OnePoint.denseRange_coe
- exists_disjoint_smul_of_isCompact
- exists_disjoint_vadd_of_isCompact
- Topology.IsClosedEmbedding.noncompactSpace
- NoncompactSpace.noncompact_univ
- TopologicalSpace.Closeds.instNoncompactSpace
- instNoncompactSpaceAdditive
- OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace
- Prod.noncompactSpace_right
- Prod.noncompactSpace_left
- OnePoint.nhdsNE_infty_neBot
- Metric.diam_univ_of_noncompact
- instNeBotCocompactOfNoncompactSpace
- OnePoint.isDenseEmbedding_coe
- instNoncompactSpaceMultiplicative
- TopologicalSpace.Compacts.instNoncompactSpace
- TopologicalSpace.NonemptyCompacts.instNoncompactSpace
- OnePoint.nhdsNE_neBot
- instNeBotCoclosedCompactOfNoncompactSpace
Ancestors0
No ancestors.