max — Mathlib

English

If f and g are maximal on s at a, then the pointwise maximum of f and g is 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. \\max\\{f(x),g(x)\\}, s, a)$$$

Lean4

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

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