no goals
ι : Type ?u.145656
ι' : Type ?u.145659
α : Type u_1
β : Type u_2
γ : Type ?u.145668
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ ∀ᶠ (x : α) in l, (fun x => -f x) x ≤ -C
simpa
no goals
ι : Type ?u.145656
ι' : Type ?u.145659
α : Type u_1
β : Type u_2
γ : Type ?u.145668
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto (fun x => (fun x => -f x) x + (fun x => f x + g x) x) l atTop
simpa