Theorems · Theorem · general topology

Metric.exists_dist_lt_of_hausdorffDist_lt

∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α} {r : ℝ},
  x ∈ s → Metric.hausdorffDist s t < r → Metric.hausdorffEDist s t ≠ ⊤ → ∃ y ∈ t, dist x y < r

If the Hausdorff distance is < r, any point in one of the sets is at distance < r of a point in the other set.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDistance

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace