Theorems · Theorem · general topology
isCompact_sphere
∀ {α : Type u_3} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ), IsCompact (Metric.sphere x r)In a proper pseudometric space, all spheres are compact.
- Defined in
- Mathlib.Topology.MetricSpace.ProperSpace
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpaceProperSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- PseudoMetricSpacestatement and proof · cited by 1,550
- IsCompactstatement · cited by 1,282
- Metric.spherestatement · cited by 371
- ProperSpacestatement and proof · cited by 190
- IsCompact.of_isClosed_subsetproof · cited by 67
- ProperSpace.isCompact_closedBallproof · cited by 40
- Metric.sphere_subset_closedBallproof · cited by 24
- Metric.isClosed_sphereproof · cited by 5
Cited by11
Results whose statement or proof uses this declaration.
- MeromorphicOn.circleIntegrable_log_normproof · cited by 11
- Topology.RelCWComplex.isCompact_cellFrontierproof · cited by 2
- divisor_sphere_support_finiteproof · cited by 2
- AnalyticAt.eventually_constant_or_nhds_le_map_nhds_auxproof · cited by 1
- AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhdsproof · cited by 1
- LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closureproof · cited by 1
- LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensionalproof · cited by 1
- Complex.norm_cderiv_ltproof · cited by 1
- Complex.circleTransformDeriv_boundproof · cited by 0
- Unitary.continuousOn_argSelfAdjointproof · cited by 0
- LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensionalproof · cited by 0