ι : Sort ?u.59705
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (edist x y)
ι : Sort ?u.59705
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ infDist x s ≤ dist x y
rw [dist_edist, infDist]
no goals
ι : Sort ?u.59705
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : y ∈ s
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (edist x y)
exact ENNReal.toReal_mono (edist_ne_top _ _) (infEdist_le_edist_of_mem h)