α : Type u
β : Type v
X : Type ?u.529537
ι : Type ?u.529540
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
⊢ ENNReal.toReal (max (max (edist x y) (edist x z)) (edist y z)) =
    max (max (ENNReal.toReal (edist x y)) (ENNReal.toReal (edist x z))) (ENNReal.toReal (edist y z))
α : Type u
β : Type v
X : Type ?u.529537
ι : Type ?u.529540
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
⊢ diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
simp only [Metric.diam, EMetric.diam_triple, dist_edist]
no goals
α : Type u
β : Type v
X : Type ?u.529537
ι : Type ?u.529540
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
⊢ ENNReal.toReal (max (max (edist x y) (edist x z)) (edist y z)) =
    max (max (ENNReal.toReal (edist x y)) (ENNReal.toReal (edist x z))) (ENNReal.toReal (edist y z))
rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]