IsMaxOn

Mathlib.Order.Filter.Extr

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

English

IsMaxOn f s a means f x ≤ f a for all x ∈ s.

Русский

IsMaxOn f s a означает, что f x ≤ f a для всех x ∈ s.

LaTeX

$$$\mathrm{IsMaxOn} = \mathrm{IsMaxFilter}(f, \mathcal{P} s, a)$$$

Lean4

/-- `IsMaxOn f s a` means that `f x ≤ f a` for all `x ∈ s`. Note that we do not assume `a ∈ s`. -/
def IsMaxOn :=
  IsMaxFilter f (𝓟 s) a

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

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

Разделы

Аффилиация

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