exact (tendsto_atTop_zero_real (compNegEquiv f)).comp Filter.tendsto_neg_atBot_atTop
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => (compNegEquiv f) (-x)) Filter.atBot (nhds 0)
no goals