sub_concaveOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sub_concaveOn (hf : StrictConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) : StrictConvexOn 𝕜 s (f - g) :=
  (sub_eq_add_neg f g).symm ▸ hf.add_convexOn hg.neg

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