isLocalExtrOn_const

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#isLocalExtrOn_const

English

For any fixed b, the constant function f(x) = b is a local extremum on any set s at any a.

Русский

Для любой константы b функция f(x) = b является локальным экстремумом на любом множестве s в любой точке a.

LaTeX

$$$IsLocalExtrOn(\lambda x. b)\ s\ a$$$

Lean4

theorem isLocalExtrOn_const {b : β} : IsLocalExtrOn (fun _ => b) s a :=
  isExtrFilter_const

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

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

Разделы

Аффилиация

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