α : Type u_1
β : Type ?u.77060
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
α : Type u_1
β : Type ?u.77060
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : Finset.offDiag s = ∅
⊢ infsep ↑s = 0
rw [← Finset.not_nonempty_iff_eq_empty] at hs
no goals
α : Type u_1
β : Type ?u.77060
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
rw [Finset.coe_infsep, dif_neg hs]