ι : Sort ?u.8332
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
⊢ edist x y ≤ ⨅ (i : α) (_ : i ∈ s), edist x i + diam s
ι : Sort ?u.8332
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
⊢ edist x y ≤ infEdist x s + diam s
simp_rw [infEdist, ENNReal.iInf_add]
ι : Sort ?u.8332
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + diam s
ι : Sort ?u.8332
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
⊢ edist x y ≤ ⨅ (i : α) (_ : i ∈ s), edist x i + diam s
refine le_iInf₂ fun i hi => ?_
no goals
ι : Sort ?u.8332
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + diam s
calc
  edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
  _ ≤ edist x i + diam s := add_le_add le_rfl (edist_le_diam_of_mem hi hy)