sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sub (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) : ConvexOn 𝕜 s (f - g) :=
  (sub_eq_add_neg f g).symm ▸ hf.add hg.neg

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