no goals
α : Type u
β : Type v
X : Type ?u.554897
ι : Type ?u.554900
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s✝ s : Set γ
ε : ℝ
hε : 0 < ε
hs : Set.Pairwise s fun x y => ε ≤ dist x y
⊢ Set.Pairwise s fun x y => ¬(x, y) ∈ {p | dist p.fst p.snd < ε}
simpa using hs