ι : Sort ?u.63481
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Bounded s
hy : y ∈ s
⊢ ENNReal.toReal (edist x y) ≤ ENNReal.toReal (infEdist x s) + ENNReal.toReal (EMetric.diam s)
ι : Sort ?u.63481
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Bounded s
hy : y ∈ s
⊢ dist x y ≤ infDist x s + diam s
rw [infDist, diam, dist_edist]
no goals
ι : Sort ?u.63481
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
hs : Bounded s
hy : y ∈ s
⊢ ENNReal.toReal (edist x y) ≤ ENNReal.toReal (infEdist x s) + ENNReal.toReal (EMetric.diam s)
exact toReal_le_add (edist_le_infEdist_add_ediam hy) (infEdist_ne_top ⟨y, hy⟩) hs.ediam_ne_top