English
HasDerivWithinAt f f' s x implies limsup of slope f x z below r on nhdsWithin excluding x.
Русский
Если есть производная внутри, лимит суп наклона меньше r в nhdsWithin за исключением точки x.
LaTeX
$$hf : HasDerivWithinAt f f' s x → hs : x ∉ s → hr : f' < r → ∀ᶠ z in 𝓝[s] x, slope f x z < r$$
Lean4
/-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ‖f'‖` the ratio
`‖f z - f x‖ / ‖z - x‖` is frequently less than `r` as `z → x+0`.
In other words, the limit inferior of this ratio as `z` tends to `x+0`
is less than or equal to `‖f'‖`. See also `HasDerivWithinAt.limsup_norm_slope_le`
for a stronger version using limit superior and any set `s`. -/
theorem liminf_right_norm_slope_le (hf : HasDerivWithinAt f f' (Ici x) x) (hr : ‖f'‖ < r) :
∃ᶠ z in 𝓝[>] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r :=
(hf.Ioi_of_Ici.limsup_norm_slope_le hr).frequently
