mul_antitone — Mathlib

English

Let R be as above. If f is monotone, g is monotone, and ∀x, f(x) ≤ 0 and ∀x, 0 ≤ g(x), then the product x ↦ f(x) · g(x) is antitone.

Русский

Пусть f и g монотонны, f(x) ≤ 0, 0 ≤ g(x) для всех x. Тогда произведение x ↦ f(x)g(x) является антитоничным.

LaTeX

$$$\text{Monotone}(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_antitone [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R]
    (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, g x ≤ 0) : Antitone (f * g) := fun _ _ h =>
  mul_le_mul_of_nonneg_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)

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