no goals
α : Type u
β : Type v
X : Type ?u.62248
ι : Type ?u.62251
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ UniformEmbedding f ↔
    Function.Injective f ∧
      UniformContinuous f ∧ ∀ (δ : ℝ), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
rw [uniformEmbedding_iff, and_comm, uniformInducing_iff]