Theorems · Inductive type · general topology
ProperSpace
(α : Type u) → [PseudoMetricSpace α] → Prop
A pseudometric space is proper if all closed balls are compact.
- Defined in
- Mathlib.Topology.MetricSpace.ProperSpace
- Cited by
- 190 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PseudoMetricSpacestatement · cited by 1,550
Cited by197
Results whose statement or proof uses this declaration.
- ValueDistribution.logCountingstatement and proof · cited by 45
- ProperSpace.isCompact_closedBallstatement and proof · cited by 40
- Function.locallyFinsuppWithin.logCountingstatement and proof · cited by 36
- Module.Basis.ofZLatticeBasisstatement and proof · cited by 36
- isCompact_spherestatement and proof · cited by 11
- Module.Basis.ofZLatticeBasis_applystatement and proof · cited by 11
- Metric.isCompact_of_isClosed_isBoundedstatement and proof · cited by 8
- Bornology.IsBounded.measure_lt_topstatement and proof · cited by 8
- Metric.cobounded_eq_cocompactstatement and proof · cited by 8
- MeasureTheory.measure_closedBall_lt_topstatement and proof · cited by 6
- tendsto_norm_cocompact_atTopstatement and proof · cited by 6
- Bornology.IsBounded.isCompact_closurestatement and proof · cited by 6