mul_const_of_neg — Mathlib

English

If f is StrictAnti and a < 0, then x ↦ f(x) · a is StrictMonotone.

Русский

Если f строго антитонична и a < 0, то x ↦ f(x) · a строго возрастает.

LaTeX

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

Lean4

theorem mul_const_of_neg [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => f x * a :=
  (strictAnti_mul_right ha).comp hf

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