sup — Mathlib

English

If two functions f and g are maximal on a set s at a with respect to a filter l, then their pointwise supremum is also maximal on s at a.

Русский

Если две функции f и g достигают максимума на множестве s в точке a относительно фильтра l, то их поэлементный супремум также достигает максимума в этой точке.

LaTeX

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

Lean4

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

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