English
Let f,g: α → β with a ∈ α and s ⊆ α. If IsLocalMaxOn f s a and IsLocalMaxOn g s a, then IsLocalMaxOn (f ∧ g) s a.
Русский
Пусть f и g имеют локальный максимум на s в a. Тогда f ∧ g имеет локальный максимум на s в a.
LaTeX
$$$\forall {f,g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; IsLocalMaxOn f s a \to IsLocalMaxOn g s a \to IsLocalMaxOn (\\lambda x. f(x) \\wedge g(x)) s a$$$
Lean4
nonrec theorem inf (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) : IsLocalMaxOn (fun x => f x ⊓ g x) s a :=
hf.inf hg