Theorems · Theorem · general topology
Metric.dist_le_diam_of_mem
∀ {α : Type u} {s : Set α} {x y : α} [inst : PseudoMetricSpace α],
Bornology.IsBounded s → x ∈ s → y ∈ s → dist x y ≤ Metric.diam sThe distance between two points in a set is controlled by the diameter of the set.
- Defined in
- Mathlib.Topology.MetricSpace.Bounded
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 154 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.
Cites8
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 · cited by 25,697
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement · cited by 1,539
- Bornology.IsBoundedstatement and proof · cited by 293
- Metric.diamstatement · cited by 74
- Bornology.IsBounded.ediam_ne_topproof · cited by 5
- Metric.dist_le_diam_of_mem'proof · cited by 2
Cited by14
Results whose statement or proof uses this declaration.
- Real.ediam_eqproof · cited by 4
- Metric.diam_sphere_eqproof · cited by 2
- BoxIntegral.unitPartition.prepartition_isSubordinateproof · cited by 1
- MeasureTheory.measurableSet_range_of_continuous_injectiveproof · cited by 1
- GromovHausdorff.hausdorffDist_optimalproof · cited by 1
- MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasureproof · cited by 1
- IsComplete.nonempty_iInter_of_nonempty_biInterproof · cited by 1
- BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_leproof · cited by 1
- GromovHausdorff.HD_candidatesBDist_leproof · cited by 1
- Metric.diam_posproof · cited by 0
- diam_stdSimplexproof · cited by 0
- Metric.hausdorffDist_le_diamproof · cited by 0