Theorems · Theorem · general topology

Monotone.tendsto_nhdsGT

∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))

A monotone map has a limit to the right of any point x, equal to sInf (f '' (Ioi x)).

Defined in

Mathlib.Topology.Order.Monotone

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyConditionallyCompleteLinearOrderTopologicalSpaceOrderTopology