neg

Mathlib.Topology.Order.LocalExtr

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

English

If IsLocalMinOn f on s at a, then IsLocalMaxOn (−f) on s at a.

Русский

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

LaTeX

$$$\\IsLocalMinOn f s a \\Rightarrow \\IsLocalMaxOn (-f) s a$$$

Lean4

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

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

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

Разделы

Аффилиация

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