sub_convexOn — Mathlib

English

If f is strictly concave on s and g is convex on s, then f − g is strictly concave on s.

Русский

Если f строго конкавна на s, а g выпукла на s, то f − g строго конкавна на s.

LaTeX

$$$StrictConcaveOn\ 𝕜\ s\ f \land ConvexOn\ 𝕜\ s\ g \Rightarrow StrictConcaveOn\ 𝕜\ s\ (f - g)$$$

Lean4

theorem sub_convexOn (hf : StrictConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : StrictConcaveOn 𝕜 s (f - g) :=
  (sub_eq_add_neg f g).symm ▸ hf.add_concaveOn hg.neg

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