add — Mathlib

English

If IsLocalMaxOn f on s at a and IsLocalMaxOn g on s at a, then their sum is a local max on s at a.

Русский

Если f и g имеют локальные максимумы на s в a, то их сумма имеет локальный максимум на s в a.

LaTeX

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

Lean4

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

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