𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atBot
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul hC hg