IsMinOn

Mathlib.Order.Filter.Extr

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

English

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

Русский

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

LaTeX

$$$\mathrm{IsMinOn} = \mathrm{IsMinFilter}(f, \mathcal{P} s, a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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