𝓕 : Type ?u.450626
𝕜 : Type ?u.450629
α : Type u_1
ι : Type ?u.450635
κ : Type ?u.450638
E : Type u_2
F : Type ?u.450644
G : Type ?u.450647
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 α
⊢ Tendsto (fun e => ‖f e / 1‖) a (𝓝 0) ↔ Tendsto (fun e => ‖f e‖) a (𝓝 0)
𝓕 : Type ?u.450626
𝕜 : Type ?u.450629
α : Type u_1
ι : Type ?u.450635
κ : Type ?u.450638
E : Type u_2
F : Type ?u.450644
G : Type ?u.450647
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 α
⊢ Tendsto f a (𝓝 1) ↔ Tendsto (fun e => ‖f e‖) a (𝓝 0)
rw [tendsto_iff_norm_tendsto_one]
no goals
𝓕 : Type ?u.450626
𝕜 : Type ?u.450629
α : Type u_1
ι : Type ?u.450635
κ : Type ?u.450638
E : Type u_2
F : Type ?u.450644
G : Type ?u.450647
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 α
⊢ Tendsto (fun e => ‖f e / 1‖) a (𝓝 0) ↔ Tendsto (fun e => ‖f e‖) a (𝓝 0)
simp only [div_one]