no goals
α✝ : Type u
β : Type v
X : Type ?u.557273
ι : Type ?u.557276
inst✝³ : PseudoMetricSpace α✝
γ : Type w
inst✝² : MetricSpace γ
x : γ
s : Set γ
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ε : ℝ
hε : 0 < ε
f : α → γ
hf : Pairwise fun x y => ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y => ¬(f x, f y) ∈ {p | dist p.fst p.snd < ε}
simpa using hf