comp_antitone — Mathlib

English

If f is locally extremal on s at a and g is antitone, then g ∘ f is locally extremal on s at a.

Русский

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

LaTeX

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

Lean4

nonrec theorem comp_antitone (hf : IsLocalExtr f a) {g : β → γ} (hg : Antitone g) : IsLocalExtr (g ∘ f) a :=
  hf.comp_antitone hg

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