neg

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#IsLocalMin.neg

English

If f has a local minimum at a, then −f has a local maximum at a.

Русский

Если у функции f в точке a локальный минимум, то у −f в той же точке локальный максимум.

LaTeX

$$$\\IsLocalMin f a \\Rightarrow \\IsLocalMax (-f) a$$$

Lean4

nonrec theorem neg (hf : IsLocalMin f a) : IsLocalMax (fun x => -f x) a :=
  hf.neg

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

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

Разделы

Аффилиация

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