sub

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#IsLocalMaxOn.sub

English

If IsLocalMaxOn f s a and IsLocalMinOn g s a, then IsLocalMaxOn (f − g) s a.

Русский

Если IsLocalMaxOn f на s в a и IsLocalMinOn g на s в a, то IsLocalMaxOn (f − g) на s в a.

LaTeX

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

Lean4

nonrec theorem sub (hf : IsLocalMaxOn f s a) (hg : IsLocalMinOn g s a) : IsLocalMaxOn (fun x => f x - g x) s a :=
  hf.sub hg

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

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

Разделы

Аффилиация

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