no goals
ι : Sort ?u.4012
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
⊢ infEdist x s < r ↔ ∃ y, y ∈ s ∧ edist x y < r
simp_rw [infEdist, iInf_lt_iff, exists_prop]