comp_mono — Mathlib

English

If f has a local minimum at a and g is monotone, then the composition g ∘ f has a local minimum at a.

Русский

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

LaTeX

$$$\mathrm{IsLocalMin}(f,a) \land \mathrm{Monotone}(g) \Rightarrow \mathrm{IsLocalMin}(g \circ f, a)$$$

Lean4

nonrec theorem comp_mono (hf : IsLocalMin f a) {g : β → γ} (hg : Monotone g) : IsLocalMin (g ∘ f) a :=
  hf.comp_mono hg

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