α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ (i : α), i ∈ Iio a → ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ (i : α), i ∈ Ioi a → ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ (a' : α), a' < a → ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ (a' : α), a' > a → ∀ᶠ (b : β) in x, f b < a'
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ Tendsto f x (𝓝 a) ↔ (∀ (a' : α), a' < a → ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ (a' : α), a' > a → ∀ᶠ (b : β) in x, f b < a'
simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ (i : α), i ∈ Iio a → ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ (i : α), i ∈ Ioi a → ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ (a' : α), a' < a → ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ (a' : α), a' > a → ∀ᶠ (b : β) in x, f b < a'
rfl