liminf_right_slope_le — Mathlib

English

If HasDerivWithinAt f f' (Ici x) x, then there exists z with (z - x)⁻¹*(‖f z‖ - ‖f x‖) < r frequently as z → x+0.

Русский

Если есть производная внутри на [x, ∞), существует частота точек, удовлетворяющих условию по инф-границе слева.

LaTeX

$$hf : HasDerivWithinAt f f' (Ici x) x → hr : ‖f'‖ < r → ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹*(‖f z‖ - ‖f x‖) < r$$

Lean4

theorem liminf_right_slope_le (hf : HasDerivWithinAt f f' (Ici x) x) (hr : f' < r) : ∃ᶠ z in 𝓝[>] x, slope f x z < r :=
  (hf.Ioi_of_Ici.limsup_slope_le' (lt_irrefl x) hr).frequently

Похожие утверждения