Theorems · Theorem · general topology

Metric.hausdorffEDist_le_of_mem_edist

∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
  (∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) → Metric.hausdorffEDist s t ≤ r

Bounding the Hausdorff edistance 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 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace