const_mul_of_nonpos — Mathlib

English

If f is monotone and a ≤ 0, then the map x ↦ a * f(x) is antitone.

Русский

Если f монотонно, а ≤ 0, то отображение x ↦ a * f(x) антимонотонно.

LaTeX

$$$\text{Monotone}(f) \land a \le 0 \Rightarrow \text{Antitone}(x \mapsto a \cdot f(x))$$$

Lean4

theorem const_mul_of_nonpos [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f)
    (ha : a ≤ 0) : Antitone fun x => a * f x :=
  (antitone_mul_left ha).comp_monotone hf

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