Theorems · Theorem · general topology

MonotoneOn.tendsto_nhdsLT

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

Defined in

Mathlib.Topology.Order.Monotone

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyConditionallyCompleteLinearOrderTopologicalSpaceOrderTopology