mul' — Mathlib

English

If f and g are monotone on a set s, then their product is monotone on s.

Русский

Если f и g монотонны на множества s, то их произведение монотонно на s.

LaTeX

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

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 : MonotoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => f x * g x) s := fun _ hx _ hy h => mul_le_mul' (hf hx hy h) (hg hx hy h)

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