Theorems · Theorem · general topology

Filter.Tendsto.eventually_le_const

∀ {α : Type u} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {l : Filter γ}
  {f : γ → α} {u v : α}, v < u → Filter.Tendsto f l (nhds v) → ∀ᶠ (a : γ) in l, f a ≤ u

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

15 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceLinearOrderClosedIciTopology