no goals
α : Type u
β : Type v
X : Type ?u.553589
ι : Type ?u.553592
inst✝² : PseudoMetricSpace α
γ : Type w
inst✝¹ : MetricSpace γ
x : γ
s : Set γ
inst✝ : MetricSpace β
f : γ → β
⊢ UniformEmbedding f ↔
    (∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ (δ : ℝ), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
rw [uniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff]