Theorems · Theorem · general topology
Metric.cthickening_subset_iUnion_closedBall_of_lt
∀ {α : Type u_2} [inst : PseudoMetricSpace α] (E : Set α) {δ δ' : ℝ},
0 < δ' → δ < δ' → Metric.cthickening δ E ⊆ ⋃ x ∈ E, Metric.closedBall x δ'- Defined in
- Mathlib.Topology.MetricSpace.Thickening
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 152 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.
Cites13
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
- LE.le.transproof · cited by 3,151
- Set.iUnionstatement · cited by 2,483
- LT.lt.leproof · cited by 2,189
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.distproof · cited by 1,539
- Metric.closedBallstatement · cited by 704
- Metric.thickeningproof · cited by 130
- Metric.cthickeningstatement · cited by 113
- Set.mem_iUnion₂proof · cited by 70
- Metric.mem_thickening_iffproof · cited by 6
Cited by2
Results whose statement or proof uses this declaration.
- blimsup_cthickening_ae_le_of_eventually_mul_le_auxproof · cited by 1
- Metric.IsCover.of_subset_cthickening_of_ltproof · cited by 0