α : Type u
β : Type v
X : Type ?u.25437
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧
            ∀ (a b : α),
              (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} → (a, b) ∈ {p | edist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
α : Type u
β : Type v
X : Type ?u.25437
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} ⊆ {p | edist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
simp only [subset_def, Prod.forall]
no goals
α : Type u
β : Type v
X : Type ?u.25437
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧
            ∀ (a b : α),
              (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} → (a, b) ∈ {p | edist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
rfl