add — Mathlib

English

If IsLocalMinOn f on s at a and IsLocalMinOn g on s at a, then their sum is a local min on s at a.

Русский

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

LaTeX

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

Lean4

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

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