ι : Sort ?u.7435
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist y s + edist x y
ι : Sort ?u.7435
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ edist x y + infEdist y s
rw [add_comm]
no goals
ι : Sort ?u.7435
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ infEdist x s ≤ infEdist y s + edist x y
exact infEdist_le_infEdist_add_edist