English
For an antitone function on Iio x, the left-hand limit exists and equals the sInf of its image on Iio x, provided the image is bounded below.
Русский
Для антитонной функции на Iio x предел слева существует и равен sInf отобраза f'' Iio x при условии ограниченности снизу образа.
LaTeX
$$$\mathrm{AntitoneOn}(f, Iio(x)) \wedge \mathrm{BddBelow}(f'' Iio(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(x))))$$$
Lean4
/-- A monotone map has a limit to the left of any point `x`, equal to `sSup (f '' (Iio x))`. -/
theorem tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) :
Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x))) :=
MonotoneOn.tendsto_nhdsLT (Mf.monotoneOn _) (Mf.map_bddAbove bddAbove_Iio)
