α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ (i : α), i < a → ∀ (i_2 : α), a < i_2 → ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ Tendsto f x (𝓝 a)
simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ (i : α), i < a → ∀ (i_2 : α), a < i_2 → ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2
exact fun l hl u => h l u hl