English
For a monotone function f defined on the open interval to the right of x, tending to the infimum of the image on Ioi x, assuming the image is bounded below.
Русский
Для монотонной f на правой окрестности точки x существование предела слева направо к sInf (f'' Ioi x), если образ ограничен снизу.
LaTeX
$$$\mathrm{MonotoneOn}(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_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α}
(Mf : MonotoneOn f (Ioi x)) (h_bdd : BddBelow (f '' Ioi x)) : Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x))) :=
MonotoneOn.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual h_bdd
