English
For an antitoneOn function on Ioi x, Tendsto holds to the right limit sInf of the image if bounded below.
Русский
Для функции AntitoneOn на Ioi x существует предел вправо к sInf образа при ограниченности снизу.
LaTeX
$$$\mathrm{AntitoneOn}(f, Ioi(x)) \wedge \mathrm{BddBelow}(f'' Ioi(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[>]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Ioi(x))))$$$
Lean4
theorem tendsto_nhdsWithin_Ioo_right {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α}
(h_nonempty : (Ioo x y).Nonempty) (Af : AntitoneOn f (Ioo x y)) (h_bdd : BddAbove (f '' Ioo x y)) :
Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioo x y))) :=
MonotoneOn.tendsto_nhdsWithin_Ioo_right h_nonempty Af.dual_right h_bdd
