min — Mathlib

English

If f and g are min-on f on s at a, then min of f and g is also min-on at a on s.

Русский

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

LaTeX

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

Lean4

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

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