English
Let f be continuous at b and differentiable on both sides of b with the left-hand derivative ≥ 0 and the right-hand derivative ≤ 0. Then b is a local maximum of f.
Русский
Пусть f непрерывна в точке b и дифференцируема слева и справа от b, причём производная слева не меньше 0, а производная справа не больше 0. Тогда b — локальный максимум функции f.
LaTeX
$$$$\\text{Let } f:\\mathbb{R}\\to\\mathbb{R},\\ b\\in\\mathbb{R},\\text{ with } f \\text{ continuous at } b. \\\\ (\\forall x\\text{ near } b, xb:\\ \\ deriv\,f(x)\\le 0) \\Rightarrow \\text{IsLocalMax}(f,b). $$$$
Lean4
/-- The First Derivative test, maximum version. -/
theorem isLocalMax_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
(h₀ : ∀ᶠ x in 𝓝[<] b, 0 ≤ deriv f x) (h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) : IsLocalMax f b :=
isLocalMax_of_deriv' h (nhdsLT_le_nhdsNE _ (by tauto)) (nhdsGT_le_nhdsNE _ (by tauto)) h₀ h₁
