English
If f is AntitoneOn on a set with left neighborhood, left/right limits exist as sInf/sSup of the image on Iio/Ioi, under bounds.
Русский
Если f антитонна на множестве с левой окрестностью, то существуют левые и правые пределы как sInf/sSup образа на Iio/Ioi при ограниченности снизу/сверху.
LaTeX
$$$\mathrm{AntitoneOn}(f, Iio(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(x))))$$$
Lean4
/-- An antitone map has a limit to the right of any point `x`, equal to `sSup (f '' (Ioi x))`. -/
theorem tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Af : Antitone f) (x : α) :
Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x))) :=
Monotone.tendsto_nhdsGT Af.dual_right x
