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