English
If two functions f and g both realize a maximum at a with respect to a filter l, then their pointwise supremum also realizes a maximum at a.
Русский
Если функции f и g достигают максимума в точке a относительно фильтра l, то их поэлементное объединение достигает максимума в той же точке.
LaTeX
$$$\\mathrm{IsMaxFilter}(f,l,a) \\land \\mathrm{IsMaxFilter}(g,l,a) \\Rightarrow \\mathrm{IsMaxFilter}(\\lambda x. f(x) \\sqcup g(x))\,l\,a$$$
Lean4
theorem sup (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x ⊔ g x) l a :=
show IsMaxFilter (fun x => f x ⊔ g x) l a from hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg
