sub_strictConvexOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sub_strictConvexOn (hf : ConcaveOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) : StrictConcaveOn 𝕜 s (f - g) :=
  (sub_eq_add_neg f g).symm ▸ hf.add_strictConcaveOn hg.neg

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