α : Type ?u.495306
β : Type ?u.495309
γ : Type ?u.495312
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
⊢ 0 ≤ sSup s - sInf s
α : Type ?u.495306
β : Type ?u.495309
γ : Type ?u.495312
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
⊢ Metric.diam s = sSup s - sInf s
rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]
α : Type ?u.495306
β : Type ?u.495309
γ : Type ?u.495312
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : BddBelow s ∧ BddAbove s
⊢ 0 ≤ sSup s - sInf s
α : Type ?u.495306
β : Type ?u.495309
γ : Type ?u.495312
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : Metric.Bounded s
⊢ 0 ≤ sSup s - sInf s
rw [Real.bounded_iff_bddBelow_bddAbove] at h
no goals
α : Type ?u.495306
β : Type ?u.495309
γ : Type ?u.495312
inst✝ : PseudoEMetricSpace α
s : Set ℝ
h : BddBelow s ∧ BddAbove s
⊢ 0 ≤ sSup s - sInf s
exact sub_nonneg.2 (Real.sInf_le_sSup s h.1 h.2)