IsExtrOn

Mathlib.Order.Filter.Extr

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

English

IsExtrOn f s a under order dual relates to the dual extremum condition.

Русский

IsExtrOn f s a в двойственном порядке соответствует двойному условию экстремума.

LaTeX

$$IsExtrOn (Function.comp OrderDual.toDual \circ f) s a$$

Lean4

/-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
def IsExtrOn : Prop :=
  IsExtrFilter f (𝓟 s) a

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

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

Разделы

Аффилиация

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