English
Let f and g map from a topological space to a semilattice with join ⊔. If f has a local maximum at a and g has a local maximum at a, then the function x ↦ f(x) ⊔ g(x) has a local maximum at a.
Русский
Пусть f и g отображают из топологического пространства в полупорядненную группу с объединением. Если f имеет локальный максимум в a и g имеет локальный максимум в a, то функция x ↦ f(x) ⊔ g(x) имеет локальный максимум в a.
LaTeX
$$$\forall {\alpha} {\beta} [TopologicalSpace(\alpha)] [SemilatticeSup(\beta)] {f,g: \alpha \to \beta} {a: \alpha},\; IsLocalMax f \\ a \\to\; IsLocalMax g \\ a \\to\; IsLocalMax (\lambda x. f(x) \vee g(x)) \\ a$$$
Lean4
nonrec theorem sup (hf : IsLocalMax f a) (hg : IsLocalMax g a) : IsLocalMax (fun x => f x ⊔ g x) a :=
hf.sup hg
