mul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The product of two monotone functions is monotone. -/
@[to_additive add /-- The sum of two monotone functions is monotone. -/
    ]
theorem mul' [MulLeftMono α] [MulRightMono α] (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x * g x :=
  fun _ _ h => mul_le_mul' (hf h) (hg h)

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