add_strictConvexOn — Mathlib

English

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

Русский

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

LaTeX

$$$\text{If } f\text{ is convex on } s\text{ and } g\text{ is strictly convex on } s,\text{ then } f+g\text{ is strictly convex on } s$$$

Lean4

theorem add_strictConvexOn (hf : ConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) : StrictConvexOn 𝕜 s (f + g) :=
  add_comm g f ▸ hg.add_convexOn hf

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