Theorems · Theorem · general topology

MonotoneOn.tendsto_nhdsWithin_Ioo_left

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

Defined in

Mathlib.Topology.Order.Monotone

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyConditionallyCompleteLinearOrderTopologicalSpaceOrderTopology