Theorems · Theorem · general topology
Metric.infDist_le_dist_of_mem
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α}, y ∈ s → Metric.infDist x s ≤ dist x yThe minimal distance to a set is bounded by the distance to any point in this set.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 150 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.
Cites11
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
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement · cited by 1,539
- ENNReal.toRealproof · cited by 859
- EDist.edistproof · cited by 735
- Metric.infDiststatement and proof · cited by 68
- ENNReal.toReal_monoproof · cited by 59
- dist_edistproof · cited by 21
- edist_ne_topproof · cited by 17
- Metric.infEDist_le_edist_of_memproof · cited by 13
Cited by13
Results whose statement or proof uses this declaration.
- EuclideanGeometry.dist_orthogonalProjection_eq_infDistproof · cited by 5
- EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eqproof · cited by 4
- Metric.hausdorffDist_le_of_mem_distproof · cited by 3
- QuotientAddGroup.norm_mk_le_normproof · cited by 2
- riesz_lemmaproof · cited by 2
- Metric.PiNatEmbed.separationproof · cited by 2
- EuclideanGeometry.Sphere.IsTangent.infDist_eq_radiusproof · cited by 2
- PiNat.exists_disjoint_cylinderproof · cited by 2
- MeasureTheory.hasDerivAt_resolventTransformproof · cited by 1
- Metric.notMem_of_dist_lt_infDistproof · cited by 1
- MeasureTheory.norm_resolvent_le_inv_infDist_supportproof · cited by 1
- Metric.infDist_inter_closedBall_of_memproof · cited by 1