mul' — Mathlib

English

The product of two strictly monotone functions is strictly monotone.

Русский

Произведение двух строго монотонных функций строго монотонно.

LaTeX

$$$StrictMono(f) \to\; StrictMono(g) \to\; StrictMono(x \mapsto f(x) \cdot g(x))$$$

Lean4

/-- The product of two strictly monotone functions is strictly monotone. -/
@[to_additive add /-- The sum of two strictly monotone functions is strictly monotone. -/
    ]
theorem mul' [MulLeftStrictMono α] [MulRightStrictMono α] (hf : StrictMono f) (hg : StrictMono g) :
    StrictMono fun x => f x * g x := fun _ _ ab => mul_lt_mul_of_lt_of_lt (hf ab) (hg ab)

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