no goals
ι : Sort ?u.5234
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ (⨅ (z : α) (_ : z ∈ s), edist y z + edist x y) = (⨅ (z : α) (_ : z ∈ s), edist y z) + edist x y
simp only [ENNReal.iInf_add]