Structures · Topology
ProperSpace
A pseudometric space is proper if all closed balls are compact.
- Defined in
- Mathlib.Topology.MetricSpace.ProperSpace
- Shape
- One type argument · adds isCompact_closedBall
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances13
- Int
- Nat
- Real
- Complex
- NNReal
- Padic
- PNat
- UpperHalfPlane
- Subtype
- Prod
- OrderDual
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by185
- ValueDistribution.logCounting
- ProperSpace.isCompact_closedBall
- Function.locallyFinsuppWithin.logCounting
- Module.Basis.ofZLatticeBasis
- Module.Basis.ofZLatticeBasis_apply
- isCompact_sphere
- Metric.cobounded_eq_cocompact
- Bornology.IsBounded.measure_lt_top
- Metric.isCompact_of_isClosed_isBounded
- Bornology.IsBounded.isCompact_closure
- Module.Basis.ofZLatticeBasis_span
- MeasureTheory.measure_closedBall_lt_top
- tendsto_norm_cocompact_atTop
- ZLattice.rank
- Function.locallyFinsuppWithin.logCounting_le
- spectrum.isCompact
- exists_pos_lt_subset_ball
- Module.Basis.ofZLatticeBasis_repr_apply
- MeasureTheory.measure_ball_lt_top
- SchwartzMap.toZeroAtInfty
- WeakDual.isCompact_of_bounded_of_closed
- IsCompact.cthickening
- Metric.finite_isBounded_inter_isClosed
- Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const
- upperHemicontinuous_spectrum
- Function.locallyFinsuppWithin.logCounting_nonneg
- quasispectrum.isCompact
- Metric.isCompact_iff_isClosed_bounded
- spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty
- isProperMap_dist
- ZLattice.module_finite
- tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding
- Metric.mem_cocompact_of_closedBall_compl_subset
- MeromorphicOn.divisor_ball_support_finite
- tendsto_subseq_of_bounded
- Metric.isCover_iff_subset_cthickening
- MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt
- SchwartzMap.isBigO_cocompact_rpow
- upperHemicontinuous_quasispectrum
- ValueDistribution.logCounting_top
- ValueDistribution.logCounting_mul_zero_le
- Polynomial.isClosedMap_eval
- ValueDistribution.logCounting_zero
- MeasureTheory.isTightMeasureSet_of_tendsto_measure_compl_closedBall
- Continuous.exists_forall_le_of_isBounded
- MeasureTheory.isTightMeasureSet_of_tendsto_measure_norm_gt
- ValueDistribution.logCounting_mul_top_le
- ZLattice.module_free
- Function.locallyFinsuppWithin.logCounting_mono
- ValueDistribution.logCounting_nonneg
Ancestors0
No ancestors.