limsup_slope_le — Mathlib

English

If HasDerivWithinAt f f' s x, then for any r > f', eventually slope f x z is less than r as z approaches x outside {x} within s.

Русский

Если HasDerivWithinAt f f' s x, то при любом r > f' существует окрестность such что для z близких к x в пределах s и не равных x, slope f x z < r.

LaTeX

$$HasDerivWithinAt f f' s x → f' < r → ∀ᶠ z in 𝓝[s \\ { x }] x, slope f x z < r$$

Lean4

theorem limsup_slope_le (hf : HasDerivWithinAt f f' s x) (hr : f' < r) : ∀ᶠ z in 𝓝[s \ { x }] x, slope f x z < r :=
  hasDerivWithinAt_iff_tendsto_slope.1 hf (IsOpen.mem_nhds isOpen_Iio hr)

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