ι : Sort ?u.65043
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hx : x ∈ closure s
⊢ infDist x (closure s) = 0
ι : Sort ?u.65043
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hx : x ∈ closure s
⊢ infDist x s = 0
rw [← infDist_closure]
no goals
ι : Sort ?u.65043
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hx : x ∈ closure s
⊢ infDist x (closure s) = 0
exact infDist_zero_of_mem hx