sup — Mathlib

English

If two functions f and g are minimal on a set s at a with respect to a filter l, then their pointwise supremum is also minimal on s at a.

Русский

Если функции f и g минимальны на множестве s в точке a относительно фильтра l, то их поэлементный супремум также минимален в этой точке.

LaTeX

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

Lean4

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

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