no goals
ι : Sort ?u.70605
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
s t u : Set α
x✝ y : α
Φ : α → β
inst✝ : ProperSpace α
hne : Set.Nonempty s
x : α
⊢ ∃ y, y ∈ closure s ∧ infDist x s = dist x y
simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x