add_const — Mathlib

English

If f is strictly convex on s, then f + const is strictly convex on s.

Русский

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

LaTeX

$$$\text{If } f\text{ is strictly convex on } s,\; f+ c\text{ is strictly convex on } s$$$

Lean4

theorem add_const {γ : Type*} {f : E → γ} [AddCommMonoid γ] [PartialOrder γ] [IsOrderedCancelAddMonoid γ] [Module 𝕜 γ]
    (hf : StrictConvexOn 𝕜 s f) (b : γ) : StrictConvexOn 𝕜 s (f + fun _ => b) :=
  hf.add_convexOn (convexOn_const _ hf.1)

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