α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
⊢ Tendsto (fun x => f x + g x) l atTop
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x + g x) l atTop
nontriviality α
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto (fun x => f x + g x) l atTop
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
⊢ Tendsto (fun x => f x + g x) l atTop
obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto (fun x => f x + g x) l atTop
refine' tendsto_atTop_add_left_of_le' _ C' _ hg
no goals
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x
exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt