Theorems · Theorem · general topology

tendsto_order

∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f : β → α} {a : α}
  {x : Filter β},
  Filter.Tendsto f x (nhds a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Defined in

Mathlib.Topology.Order.Basic

Cited by

60 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpacePreorderOrderTopology