no goals
𝓕 : Type ?u.107897
𝕜 : Type ?u.107900
α : Type u_1
ι : Type ?u.107906
κ : Type ?u.107909
E : Type u_2
F : Type ?u.107915
G : Type ?u.107918
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
l : Filter α
⊢ (∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, dist (f x) 1 < ε) ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : α) in l, ‖f x‖ < ε
simp only [dist_one_right]