neg_strictConcaveOn_iff — Mathlib

English

A function -f is strictly concave on s iff f is strictly convex on s.

Русский

Функция -f строго конкавна на s тогда и только тогда, когда f строго выпукла на s.

LaTeX

$$$StrictConcaveOn\ 𝕜\ s\ (-f) \iff StrictConvexOn\ 𝕜\ s\ f$$$

Lean4

/-- A function `-f` is strictly concave iff `f` is strictly convex. -/
@[simp]
theorem neg_strictConcaveOn_iff : StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f := by
  rw [← neg_strictConvexOn_iff, neg_neg f]

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