English
A monotone function f on the left side of x has a left limit at x equal to the supremum-like bound sInf of its left image.
Русский
У монотонной функции f слева от x есть левый предел в x, равный sInf образа f(Iio x).
LaTeX
$$$\mathrm{MonotoneOn}(f, Iio(x)) \Rightarrow \mathrm{Tendsto}\, f\,(\mathcal{N}_{[<]}(x))\,(\mathcal{N}(\mathrm{sInf}(f'' Iio(x))))$$$
Lean4
/-- A monotone map has a limit to the right of any point `x`, equal to `sInf (f '' (Ioi x))`. -/
theorem tendsto_nhdsGT {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
[ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} (Mf : Monotone f) (x : α) :
Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x))) :=
Monotone.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual x
