theorem abs_infDist_sub_infDist_le_dist {α : Type u} [PseudoMetricSpace α] {C : Set α} (x y : α) : |Metric.infDist x C - Metric.infDist y C| ≤ dist x y

Example 1.48: the textbook estimate (1.67) is the pointwise form of the canonical 1-Lipschitz estimate for x ↦ Metric.infDist x C; the book's nonemptiness hypothesis is unnecessary for this inequality.