mul_antitone' — Mathlib

English

If f is strictly antitone and g is antitone, then x ↦ f(x)·g(x) is strictly antitone.

Русский

Если f строго антитонна и g антитонна, то x ↦ f(x)·g(x) строго антитонно.

LaTeX

$$$StrictAnti(f) \land Antitone(g) \Rightarrow StrictAnti(\lambda x. f(x) \cdot g(x))$$$

Lean4

/-- The product of a strictly antitone function and an antitone function is strictly antitone. -/
@[to_additive add_antitone /-- The sum of a strictly antitone function and an antitone function is
    strictly antitone. -/
    ]
theorem mul_antitone' (hf : StrictAnti f) (hg : Antitone g) : StrictAnti fun x => f x * g x := fun _ _ h =>
  mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

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