const_mul_of_neg — Mathlib

English

If f is strictly monotone and a < 0, then x ↦ a · f(x) is strictly decreasing.

Русский

Если f строго монотонна и a < 0, то x → a · f(x) строго убывает.

LaTeX

$$$\text{StrictMono}(f) \wedge a < 0 \Rightarrow \text{StrictAnti}(x \mapsto a \cdot f(x))$$$

Lean4

theorem const_mul_of_neg [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => a * f x :=
  (strictAnti_mul_left ha).comp_strictMono hf

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