inf — Mathlib

English

If f and g are minimal on s at a, then their pointwise infimum is minimal on s at a.

Русский

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

LaTeX

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

Lean4

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

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