add

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsMinOn.add

English

If f and g are both minimal on s at a, then f + g is minimal on s at a.

Русский

Если f и g оба минимальны на s в точке a, то сумма f + g минимальна на s в точке a.

LaTeX

$$$hf : IsMinOn f s a \;\; hg : IsMinOn g s a \Rightarrow IsMinOn (\lambda x. f x + g x) s a$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru