α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i
⊢ ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, g a ∈ Ioi i
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ᶠ[l] g
⊢ Tendsto g l (𝓝 ⊤)
simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i
⊢ ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, g a ∈ Ioi i
intro x hx
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β), i < ⊤ → ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le