English
Let R be a semiring with preorder, and f, g: α → R with f antitone and g monotone. If ∀x, f(x) ≤ 0 and ∀x, 0 ≤ g(x), then the product x ↦ f(x) · g(x) is antitone.
Русский
Пусть f — антитонична, g — монотонна; если для всех x выполняются f(x) ≤ 0 и 0 ≤ g(x), то произведение f(x)g(x) как функция от x является антитоничной.
LaTeX
$$$\text{Antitone}(f) \wedge \text{Monotone}(g) \wedge (\forall x\, f(x) \le 0) \wedge (\forall x\, 0 \le g(x)) \Rightarrow \text{Antitone}(x \mapsto f(x)\,g(x))$$$
Lean4
theorem mul_monotone [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R]
(hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ x, f x ≤ 0) (hg₀ : ∀ x, 0 ≤ g x) : Antitone (f * g) := fun _ _ h =>
mul_le_mul_of_nonpos_of_nonneg (hf h) (hg h) (hf₀ _) (hg₀ _)
