ι : Sort ?u.61351
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (infEdist y s) + ENNReal.toReal (edist x y)
ι : Sort ?u.61351
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infDist x s ≤ infDist y s + dist x y
rw [infDist, infDist, dist_edist]
ι : Sort ?u.61351
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infEdist y s = ⊤ → infEdist x s = ⊤
ι : Sort ?u.61351
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ ENNReal.toReal (infEdist x s) ≤ ENNReal.toReal (infEdist y s) + ENNReal.toReal (edist x y)
refine ENNReal.toReal_le_add' infEdist_le_infEdist_add_edist ?_ (flip absurd (edist_ne_top _ _))
no goals
ι : Sort ?u.61351
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
⊢ infEdist y s = ⊤ → infEdist x s = ⊤
simp only [infEdist_eq_top_iff, imp_self]