sup — Mathlib

English

Let f,g: α → β, with a ∈ s where s ⊆ α. If IsLocalMinOn f s a and IsLocalMinOn g s a, then IsLocalMinOn (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},\; IsLocalMinOn f s a \to IsLocalMinOn g s a \to IsLocalMinOn (\\lambda x. f(x) \\vee g(x)) s a$$$

Lean4

nonrec theorem sup (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) : IsLocalMinOn (fun x => f x ⊔ g x) s a :=
  hf.sup hg

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