α : Type u_1
β : Type ?u.430325
γ : Type ?u.430328
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
⊢ edist x y ≤ diam s
α : Type u_1
β : Type ?u.430325
γ : Type ?u.430328
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ diam (closure s) = diam s
refine' le_antisymm (diam_le fun x hx y hy => _) (diam_mono subset_closure)
α : Type u_1
β : Type ?u.430325
γ : Type ?u.430328
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
this : edist x y ∈ closure (Iic (diam s))
⊢ edist x y ≤ diam s
α : Type u_1
β : Type ?u.430325
γ : Type ?u.430328
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
⊢ edist x y ≤ diam s
have : edist x y ∈ closure (Iic (diam s)) :=
  map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_diam_of_mem hx hy
no goals
α : Type u_1
β : Type ?u.430325
γ : Type ?u.430328
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
this : edist x y ∈ closure (Iic (diam s))
⊢ edist x y ≤ diam s
rwa [closure_Iic] at this