inf — Mathlib

English

Let f,g: α → β with a ∈ α and s ⊆ α. If IsLocalMaxOn f s a and IsLocalMaxOn g s a, then IsLocalMaxOn (x ↦ f(x) ⊓ g(x)) s a.

Русский

Пусть f,g: α → β, a ∈ α, s ⊆ α. Если 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 : IsLocalMax f a) (hg : IsLocalMax g a) : IsLocalMax (fun x => f x ⊓ g x) a :=
  hf.inf hg

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