neg

Mathlib.Topology.Order.LocalExtr

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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