Theorems · Theorem · general topology

Metric.infDist_lt_iff

∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ},
  s.Nonempty → (Metric.infDist x s < r ↔ ∃ y ∈ s, dist x y < r)

The minimal distance to a set s is < r iff there exists a point in s at distance < r.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDistance

Cited by

4 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace