no goals
α : Type u
β : Type v
X : Type ?u.60022
ι : Type ?u.60025
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | dist p.fst p.snd < i} ⊆ {p | dist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod_map, mem_setOf]