Theorems · Theorem · general topology

Metric.hausdorffDist_le_of_mem_dist

∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {r : ℝ},
  0 ≤ r → (∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) → Metric.hausdorffDist s t ≤ r

Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance

Defined in

Mathlib.Topology.MetricSpace.HausdorffDistance

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace