nonpos_of_antitoneOn — Mathlib

English

If an antitone function g has a derivative within s at x, then the derivative is nonpositive: derivWithin g s x ≤ 0.

Русский

Если функция g антонитонна на s и имеет производную внутри s в точке x, то эта производная неотрицательно не больше нуля: derivWithin g s x ≤ 0.

LaTeX

$$AccPt x (𝓟 s) ∧ HasDerivWithinAt g g' s x ∧ AntitoneOn g s ⇒ g' ≤ 0$$

Lean4

/-- If an antitone function has a derivative within a set at a non-isolated point, then this
derivative is nonpositive. -/
theorem nonpos_of_antitoneOn (hx : AccPt x (𝓟 s)) (hd : HasDerivWithinAt g g' s x) (hg : AntitoneOn g s) : g' ≤ 0 :=
  by
  have : MonotoneOn (-g) s := fun x hx y hy hxy ↦ by simpa using hg hx hy hxy
  simpa using hd.neg.nonneg_of_monotoneOn hx this

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