comp_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 comp_mono (hf : IsLocalMaxOn f s a) {g : β → γ} (hg : Monotone g) : IsLocalMaxOn (g ∘ f) s a :=
  hf.comp_mono hg

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