add — Mathlib

English

If f and g each have a local maximum at a, then x ↦ f(x) + g(x) has a local maximum at a.

Русский

Если у функций f и g в точке a имеется локальный максимум, то их сумма имеет локальный максимум в a.

LaTeX

$$$\\IsLocalMax f a \\land \\IsLocalMax g a \\Rightarrow \\IsLocalMax (x \\mapsto f(x) + g(x)) a$$$

Lean4

nonrec theorem add (hf : IsLocalMax f a) (hg : IsLocalMax g a) : IsLocalMax (fun x => f x + g x) a :=
  hf.add hg

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