case h.e'_2.a
𝓕 : Type ?u.448410
𝕜 : Type ?u.448413
α : Type u_1
ι : Type ?u.448419
κ : Type ?u.448422
E : Type u_2
F : Type ?u.448428
G : Type ?u.448431
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
a : Filter α
b : E
⊢ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) ↔ Tendsto (fun b_1 => dist (f b_1) b) a (𝓝 0)
𝓕 : Type ?u.448410
𝕜 : Type ?u.448413
α : Type u_1
ι : Type ?u.448419
κ : Type ?u.448422
E : Type u_2
F : Type ?u.448428
G : Type ?u.448431
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0)
convert tendsto_iff_dist_tendsto_zero (f := f) (x := a) (a := b) using 1
no goals
case h.e'_2.a
𝓕 : Type ?u.448410
𝕜 : Type ?u.448413
α : Type u_1
ι : Type ?u.448419
κ : Type ?u.448422
E : Type u_2
F : Type ?u.448428
G : Type ?u.448431
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a✝ a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
f : α → E
a : Filter α
b : E
⊢ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) ↔ Tendsto (fun b_1 => dist (f b_1) b) a (𝓝 0)
simp [dist_eq_norm_div]