English
An antitone function on the left side yields a left-limit equal to sInf of the image on Iio x, under a lower bound.
Русский
Антитонная функция слева от x имеет левый предел, равный sInf образа на Iio x при условии нижней границы.
LaTeX
$$$\mathrm{Antitone}(f) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(x))))$$$
Lean4
theorem tendsto_nhdsLT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
(Af : AntitoneOn f (Iio x)) (h_bdd : BddBelow (f '' Iio x)) : Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x))) :=
MonotoneOn.tendsto_nhdsLT Af.dual_right h_bdd
