mul_const_of_nonpos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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