no goals
α : Type u
β✝ : Type v
X : Type ?u.559730
ι : Type ?u.559733
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s : Set γ
β : Type ?u.559749
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y => ε ≤ dist (f x) (f y)
⊢ UniformSpace α
infer_instance
no goals
α : Type u
β✝ : Type v
X : Type ?u.559730
ι : Type ?u.559733
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s : Set γ
β : Type u_1
ε : ℝ
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