English
Let f: α → β be monotone, with α a linear order and β a topological ConditionallyCompleteLinearOrder. Then f is continuous from the right at x along (x, ∞) if and only if the right-hand limit of f at x equals f(x).
Русский
Пусть f: α → β монотонна; α упорядочена линейно, β — топологическое упорядоченное литературное пространство с условной полнотой. Тогда функция непрерывна справа в точке x вдоль (x, ∞) тогда и только когда правый предел в x равен f(x).
LaTeX
$$$\text{ContinuousWithinAt}(f,\,\mathrm{Ioi}(x),\,x) \iff \operatorname{rightLim} f x = f x$$$
Lean4
/-- A monotone function is continuous to the right at a point if and only if its right limit
coincides with the value of the function. -/
theorem continuousWithinAt_Ioi_iff_rightLim_eq : ContinuousWithinAt f (Ioi x) x ↔ rightLim f x = f x :=
hf.dual.continuousWithinAt_Iio_iff_leftLim_eq
