inf

Mathlib.Order.Filter.Extr

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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