α : Type ?u.57289
β : Type ?u.57292
ι✝ : Type ?u.57295
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup 𝔸
inst✝ : NormedSpace 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : ε =o[l] fun _x => 1
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x => 1
α : Type ?u.57289
β : Type ?u.57292
ι✝ : Type ?u.57295
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup 𝔸
inst✝ : NormedSpace 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)
rw [← isLittleO_one_iff 𝕜] at hε⊢
no goals
α : Type ?u.57289
β : Type ?u.57292
ι✝ : Type ?u.57295
ι : Type u_1
𝕜 : Type u_2
𝔸 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup 𝔸
inst✝ : NormedSpace 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : ε =o[l] fun _x => 1
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x => 1
simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))