max — Mathlib

English

If two functions f and g are maximal on s at a, then their pointwise maximum is also maximal on s at a.

Русский

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

LaTeX

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

Lean4

theorem max (hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => max (f x) (g x)) s a :=
  IsMinFilter.max hf hg

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