Structures · Topology
WeaklyLocallyCompactSpace
We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.
- Defined in
- Mathlib.Topology.Defs.Filter
- Shape
- One type argument · adds exists_compact_mem_nhds
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances10
- DomMulAct
- Units
- RestrictedProduct
- DomAddAct
- AddUnits
- Prod
- MulOpposite
- AddOpposite
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by64
- WeaklyLocallyCompactSpace.exists_compact_mem_nhds
- FiniteDimensional.of_locallyCompactSpace
- exists_compact_superset
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
- MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le
- MeasureTheory.measure_univ_of_isAddLeftInvariant
- MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
- Metric.exists_isCompact_closedBall
- exists_mem_nhds_isCompact_isClosed
- MeasureTheory.measure_univ_of_isMulLeftInvariant
- Continuous.discrete_of_tendsto_cofinite_cocompact
- CompactExhaustion.choice
- Metric.eventually_isCompact_closedBall
- ContinuousMap.exists_tendsto_compactOpen_iff_forall
- isCompact_isClosed_basis_nhds
- MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le
- exists_isOpen_superset_and_isCompact_closure
- Topology.IsClosedEmbedding.weaklyLocallyCompactSpace
- ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace
- RestrictedProduct.weaklyLocallyCompactSpace_of_principal
- MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le
- OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space
- DomAddAct.instWeaklyLocallyCompactSpace
- IsRightUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace
- CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace
- RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite
- SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace
- MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le
- MeasureTheory.Content.regular
- ContinuousMap.tendsto_iff_tendstoLocallyUniformly
- ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace
- disjoint_nhds_cocompact
- MulOpposite.instWeaklyLocallyCompactSpace
- IsClosed.tendsto_coe_cofinite_iff
- MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts
- MeasureTheory.Measure.IsAddHaarMeasure.nullSingletonClass
- instWeaklyLocallyCompactSpaceProd
- Units.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul
- MeasureTheory.Measure.IsHaarMeasure.nullSingletonClass
- Continuous.tendstoUniformly
- instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace
- ContinuousMap.instPseudoMetrizableSpace
- RestrictedProduct.instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem
- RestrictedProduct.instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem
- instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space
- instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space
- IsClosed.weaklyLocallyCompactSpace
- TopologicalSpace.PositiveCompacts.nonempty'
- IsRightUniformGroup.completeSpace_of_weaklyLocallyCompactSpace
- refinement_of_locallyCompact_sigmaCompact_of_nhds_basis
Ancestors0
No ancestors.