min — Mathlib

English

If f and g are minimal with respect to l at a, then the pointwise minimum of f and g is minimal at a.

Русский

Если f и g минимальны относительно l в a, то поэлементное минимальное значение минимально в a.

LaTeX

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

Lean4

theorem min (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => min (f x) (g x)) l a :=
  show IsMinFilter (fun x => Min.min (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => min_le_min hx hy) hg

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