add

Mathlib.Order.Filter.Extr

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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