bicomp_mono — Mathlib

English

If f has a local maximum on s at a and g is antitone, then g ∘ f has a local minimum on s at a.

Русский

Если f имеет локальный максимум на s в a, а g антитонна, то g ∘ f имеет локальный минимум на s в a.

LaTeX

$$$\mathrm{IsLocalMaxOn}(f,s,a) \land \mathrm{Antitone}(g) \Rightarrow \mathrm{IsLocalMinOn}(g \circ f, s, a)$$$

Lean4

nonrec theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op)
    (hf : IsLocalMax f a) {g : α → γ} (hg : IsLocalMax g a) : IsLocalMax (fun x => op (f x) (g x)) a :=
  hf.bicomp_mono hop hg

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