min

Mathlib.Order.Filter.Extr

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

English

If f and g are maximal on s at a, then their minimum is also maximal at a.

Русский

Если f и g максимальны на s в a, то их минимум максимален в a.

LaTeX

$$$\\mathrm{IsMaxOn}(f,s,a) \\land \\mathrm{IsMaxOn}(g,s,a) \\Rightarrow \\mathrm{IsMaxOn}(\\lambda x. \\min\\{f(x),g(x)\\}, s, a)$$$

Lean4

theorem min (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => min (f x) (g x)) s a :=
  IsMaxFilter.min hf hg

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

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

Разделы

Аффилиация

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