mul_monotone' — Mathlib

English

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

Русский

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

LaTeX

$$$StrictMono(f) \land Monotone(g) \Rightarrow StrictMono(x \mapsto f(x) \cdot g(x))$$$

Lean4

/-- The product of a strictly monotone function and a monotone function is strictly monotone. -/
@[to_additive add_monotone /-- The sum of a strictly monotone function and a monotone function is
    strictly monotone. -/
    ]
theorem mul_monotone' (hf : StrictMono f) (hg : Monotone g) : StrictMono fun x => f x * g x := fun _ _ h =>
  mul_lt_mul_of_lt_of_le (hf h) (hg h.le)

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