English
Let x < y in a linearly ordered space with the order topology. The derivative of f at x within the interval (x, y) exists with value f' if and only if the derivative of f at x within the right-hand interval (x, ∞) exists with the same value f'.
Русский
Пусть x < y в линейно упорядоченном пространстве с топологией порядка. Производная функции f в точке x внутри интервала (x, y) существует и равна f', тогда и только тогда существует производная внутри правого полупространства (x, ∞) с той же величиной f'.
LaTeX
$$$\text{HasDerivWithinAt } f\; f'\; (Ioo(x,y))\; x \;\iff\; \text{HasDerivWithinAt } f\; f'\; (Ioi(x))\; x$$$
Lean4
theorem Ioi_iff_Ioo [LinearOrder 𝕜] [OrderClosedTopology 𝕜] {x y : 𝕜} (h : x < y) :
HasDerivWithinAt f f' (Ioo x y) x ↔ HasDerivWithinAt f f' (Ioi x) x :=
hasFDerivWithinAt_inter <| Iio_mem_nhds h
