Theorems · Theorem · general topology

Metric.infDist_le_infDist_add_hausdorffDist

∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
  Metric.hausdorffEDist s t ≠ ⊤ → Metric.infDist x t ≤ Metric.infDist x s + Metric.hausdorffDist s t

The infimum distance to s and t are the same, up to the Hausdorff distance between s and t

Defined in

Mathlib.Topology.MetricSpace.HausdorffDistance

Cited by

1 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace