no goals
α : Type u
β : Type v
X : Type ?u.310325
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : EMetricSpace β
f : γ → β
⊢ UniformEmbedding f ↔
    (∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
rw [uniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff]