English
Let f and g be functions from a topological space into a semilattice with join ⊔. If f has a local minimum at a and g has a local minimum at a, then the pointwise supremum x ↦ f(x) ⊔ g(x) also has a local minimum at a.
Русский
Пусть f и g — функции из топологического пространства в полупорядоченную группу с операцией объединения sup (⊔). Если 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},\; IsLocalMin f \\ a \; \to\; IsLocalMin g \\ a \; \to\; IsLocalMin (\lambda x. f(x) \vee g(x)) \\ a$$$
Lean4
nonrec theorem sup (hf : IsLocalMin f a) (hg : IsLocalMin g a) : IsLocalMin (fun x => f x ⊔ g x) a :=
hf.sup hg
