English
Let g be monotone on s. If g is differentiable within s at x, then the derivative within s at x is nonnegative: 0 ≤ derivWithin g s x.
Русский
Пусть g монотонна на s. Если g дифференцируема внутри s в точке x, то производная внутри s в x неотрицательна: 0 ≤ derivWithin g s x.
LaTeX
$$$MonotoneOn(g,s) \\rightarrow 0 \\le \\derivWithin g\\ s\\ x$$$
Lean4
/-- The derivative within a set of a monotone function is nonnegative. -/
theorem derivWithin_nonneg (hg : MonotoneOn g s) : 0 ≤ derivWithin g s x :=
by
by_cases hd : DifferentiableWithinAt 𝕜 g s x; swap
· simp [derivWithin_zero_of_not_differentiableWithinAt hd]
by_cases hx : AccPt x (𝓟 s); swap
· simp [derivWithin_zero_of_not_accPt hx]
exact hd.hasDerivWithinAt.nonneg_of_monotoneOn hx hg
