α : Type u
β : Type v
X : Type ?u.532598
ι : Type ?u.532601
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ ENNReal.toReal (edist x y) ≤ ENNReal.toReal (EMetric.diam s)
α : Type u
β : Type v
X : Type ?u.532598
ι : Type ?u.532601
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ diam s
rw [diam, dist_edist]
α : Type u
β : Type v
X : Type ?u.532598
ι : Type ?u.532601
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ edist x y ≤ EMetric.diam s
α : Type u
β : Type v
X : Type ?u.532598
ι : Type ?u.532601
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ ENNReal.toReal (edist x y) ≤ ENNReal.toReal (EMetric.diam s)
rw [ENNReal.toReal_le_toReal (edist_ne_top _ _) h]
no goals
α : Type u
β : Type v
X : Type ?u.532598
ι : Type ?u.532601
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
h : EMetric.diam s ≠ ⊤
hx : x ∈ s
hy : y ∈ s
⊢ edist x y ≤ EMetric.diam s
exact EMetric.edist_le_diam_of_mem hx hy