English
For an antitoneOn f on Iio x, f'' Iio x bounded above implies Tendsto to sInf of image from the left.
Русский
Для антитонной On f на Iio x, если образ ограничен сверху, то f стремится к sInf образа слева.
LaTeX
$$$\mathrm{AntitoneOn}(f, Iio(x)) \wedge \mathrm{BddAbove}(f'' Iio(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(x))))$$$
Lean4
theorem tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α}
(h_nonempty : (Ioo y x).Nonempty) (Af : AntitoneOn f (Ioo y x)) (h_bdd : BddBelow (f '' Ioo y x)) :
Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Ioo y x))) :=
MonotoneOn.tendsto_nhdsWithin_Ioo_left h_nonempty Af.dual_right h_bdd
