Theorems · Definition · general topology
Metric.cthickening
{α : Type u} → [PseudoEMetricSpace α] → ℝ → Set α → Set αThe closed δ-thickening Metric.cthickening δ E of a subset E in a pseudo emetric space
consists of those points that are at infimum distance at most δ from E.
- Defined in
- Mathlib.Topology.MetricSpace.Thickening
- Cited by
- 113 results in Mathlib
- Foundations
- Depth 148 from the axioms, rests on 3,163 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.ofPredproof · cited by 6,101
- PseudoEMetricSpacestatement and proof · cited by 1,536
- ENNReal.ofRealproof · cited by 863
- Metric.infEDistproof · cited by 147
Cited by113
Results whose statement or proof uses this declaration.
- Metric.thickening_subset_cthickeningstatement · cited by 12
- Metric.cthickening_of_nonposstatement · cited by 8
- Metric.cthickening_zerostatement · cited by 8
- TendstoLocallyUniformlyOn.differentiableOnproof · cited by 7
- Metric.closedBall_subset_cthickeningstatement · cited by 6
- Metric.cthickening_monostatement · cited by 6
- Metric.cthickening_subset_thickening'statement and proof · cited by 6
- IsCompact.add_closedBall_zerostatement · cited by 5
- Metric.isClosed_cthickeningstatement · cited by 5
- IsCompact.exists_thickening_subset_openproof · cited by 5
- IsCompact.cthickeningstatement · cited by 4
- IsCompact.exists_cthickening_subset_openstatement and proof · cited by 4