no goals
𝓕 : Type ?u.108981
𝕜 : Type ?u.108984
α : Type ?u.108987
ι : Type ?u.108990
κ : Type ?u.108993
E : Type u_1
F : Type u_2
G : Type ?u.109002
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε
simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_div]