mul_const_of_nonpos — Mathlib

English

Let R be as above and f: α → R be antitone. If a ≤ 0, then the map x ↦ f(x) · a is monotone on α.

Русский

Пусть R удовлетворяет условиям выше, f: α → R антитонична. При a ≤ 0 отображение x ↦ f(x) · a монотонно по α.

LaTeX

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

Lean4

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

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