Theorems · Theorem · general topology
Metric.cthickening_singleton
∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) {δ : ℝ}, 0 ≤ δ → Metric.cthickening δ {x} = Metric.closedBall x δ- Defined in
- Mathlib.Topology.MetricSpace.Thickening
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- Set.extproof · cited by 2,266
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.distproof · cited by 1,539
- ENNReal.ofRealproof · cited by 863
- Metric.closedBallstatement · cited by 704
- Metric.cthickeningstatement · cited by 113
- edist_distproof · cited by 39
- ENNReal.ofReal_le_ofReal_iffproof · cited by 20
- Metric.infEDist_singletonproof · cited by 4
Cited by4
Results whose statement or proof uses this declaration.
- thickening_closedBallproof · cited by 3
- Metric.closedBall_subset_cthickening_singletonproof · cited by 1
- cthickening_closedBallproof · cited by 1
- cthickening_ballproof · cited by 0