derivWithin_nonpos — Mathlib

English

If HasDerivWithinAt g g' s x and AntitoneOn g s, then g' ≤ 0 whenever x is an accumulation point of s.

Русский

Если HasDerivWithinAt g g' s x и AntitoneOn g s, то при x, являющемся предельной точкой множества s, выполняется g' ≤ 0.

LaTeX

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

Lean4

/-- The derivative within a set of an antitone function is nonpositive. -/
theorem derivWithin_nonpos (hg : AntitoneOn g s) : derivWithin g s x ≤ 0 := by
  simpa [derivWithin.fun_neg] using hg.neg.derivWithin_nonneg

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