Theorems · Theorem · general topology

Filter.Tendsto.eventually_const_le

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

Defined in

Mathlib.Topology.Order.OrderClosed

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderClosedIicTopology