hasFDerivWithinAt_eq_zero — Mathlib

English

If a and its opposite directions lie in pos tangent cone, then the derivative equals zero.

Русский

Если y и -y лежат в pos tangent cone, то производная равна нулю.

LaTeX

$$$ y \\in posTangentConeAt s a \\land -y \\in posTangentConeAt s a \\Rightarrow f' y = 0$$$

Lean4

/-- If `f` has a local max on `s` at `a`, `f'` is a derivative of `f` at `a` within `s`, and
both `y` and `-y` belong to the positive tangent cone of `s` at `a`, then `f' y ≤ 0`. -/
theorem hasFDerivWithinAt_eq_zero (h : IsLocalMaxOn f s a) (hf : HasFDerivWithinAt f f' s a)
    (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) : f' y = 0 :=
  le_antisymm (h.hasFDerivWithinAt_nonpos hf hy) <| by simpa using h.hasFDerivWithinAt_nonpos hf hy'

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