Theorems · Theorem · general topology

AntitoneOn.tendsto_nhdsLT

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

Defined in

Mathlib.Topology.Order.Monotone

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopologyConditionallyCompleteLinearOrderTopologicalSpaceOrderTopology