English
If f and g are antitone and ∀x, f(x) ≤ 0 and ∀x, g(x) ≤ 0, then the product x ↦ f(x) · g(x) is monotone.
Русский
Если f и g антитоничны и для всех x выполняется f(x) ≤ 0 и g(x) ≤ 0, то произведение x ↦ f(x)g(x) монотонно.
LaTeX
$$$\text{Antitone}(f) \wedge \text{Antitone}(g) \wedge (\forall x, f(x) \le 0) \wedge (\forall x, g(x) \le 0) \Rightarrow \text{Monotone}(x \mapsto f(x) g(x))$$$
Lean4
theorem mul [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f)
(hg : Antitone g) (hf₀ : ∀ x, f x ≤ 0) (hg₀ : ∀ x, g x ≤ 0) : Monotone (f * g) := fun _ _ h =>
mul_le_mul_of_nonpos_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)
