add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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