IsLocalExtr

Mathlib.Topology.Order.LocalExtr

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

English

IsLocalExtr f a denotes that a is a local minimum or a local maximum of f at a.

Русский

IsLocalExtr f a означает, что в точке a функция f достигает локального минимума или локального максимума.

LaTeX

$$$IsLocalExtr f a$$$

Lean4

/-- `IsLocalExtr f s a` means `IsLocalMin f s a ∨ IsLocalMax f s a`. -/
def IsLocalExtr :=
  IsExtrFilter f (𝓝 a) a

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

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

Разделы

Аффилиация

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