nonpos_of_antitone — Mathlib

English

If HasDerivAt g g' x and g is antitone, then g' ≤ 0.

Русский

Если HasDerivAt g g' x и функция g антонитонна, то производная g' не положительна: g' ≤ 0.

LaTeX

$$HasDerivAt g g' x → Antitone g → g' ≤ 0$$

Lean4

/-- If an antitone function has a derivative, then this derivative is nonpositive. -/
theorem nonpos_of_antitone (hd : HasDerivAt g g' x) (hg : Antitone g) : g' ≤ 0 :=
  by
  rw [← hasDerivWithinAt_univ] at hd
  apply hd.nonpos_of_antitoneOn _ (hg.antitoneOn _)
  exact PerfectSpace.univ_preperfect _ (mem_univ _)

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