no goals
α : Type u
β : Type v
X : Type ?u.314348
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
⊢ 0 < diam s ↔ Set.Nontrivial s
simp only [pos_iff_ne_zero, Ne.def, diam_eq_zero_iff, Set.not_subsingleton_iff]