𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
⊢ Tendsto d l (𝓝 0)
have A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0) := tendsto_inv_atTop_zero.comp hc
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
have B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖) := (continuous_norm.tendsto _).comp hd
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 (0 * ‖y‖))
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
⊢ Tendsto d l (𝓝 0)
have C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 (0 * ‖y‖)) := A.mul B
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 (0 * ‖y‖))
⊢ Tendsto d l (𝓝 0)
rw [MulZeroClass.zero_mul] at C
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
have : ∀ᶠ n in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖ := by
  refine (eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn => ?_
  rw [norm_smul, ← mul_assoc, inv_mul_cancel, one_mul]
  rwa [Ne.def, norm_eq_zero]
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
⊢ Tendsto d l (𝓝 0)
have D : Tendsto (fun n => ‖d n‖) l (𝓝 0) := Tendsto.congr' this C
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto (fun e => ‖d e‖) l (𝓝 0)
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto d l (𝓝 0)
rw [tendsto_zero_iff_norm_tendsto_zero]
no goals
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
this : ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
D : Tendsto (fun n => ‖d n‖) l (𝓝 0)
⊢ Tendsto (fun e => ‖d e‖) l (𝓝 0)
exact D
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
n : α
hn : c n ≠ 0
⊢ ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
⊢ ∀ᶠ (n : α) in l, ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
refine (eventually_ne_of_tendsto_norm_atTop hc 0).mono fun n hn => ?_
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
n : α
hn : c n ≠ 0
⊢ ‖c n‖ ≠ 0
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
n : α
hn : c n ≠ 0
⊢ ‖c n‖⁻¹ * ‖c n • d n‖ = ‖d n‖
rw [norm_smul, ← mul_assoc, inv_mul_cancel, one_mul]
no goals
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.21028
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.21118
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
α : Type u_1
l : Filter α
c : α → 𝕜
d : α → E
hc : Tendsto (fun n => ‖c n‖) l atTop
hd : Tendsto (fun n => c n • d n) l (𝓝 y)
A : Tendsto (fun n => ‖c n‖⁻¹) l (𝓝 0)
B : Tendsto (fun n => ‖c n • d n‖) l (𝓝 ‖y‖)
C : Tendsto (fun n => ‖c n‖⁻¹ * ‖c n • d n‖) l (𝓝 0)
n : α
hn : c n ≠ 0
⊢ ‖c n‖ ≠ 0
rwa [Ne.def, norm_eq_zero]