mul' — Mathlib

English

If hf and hg are strictly monotone on s, then x ↦ f(x) · g(x) is strictly monotone on s.

Русский

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

LaTeX

$$$hf: StrictMonoOn(f,s) \; \&\; hg: StrictMonoOn(g,s) \Rightarrow \; StrictMonoOn(\lambda x. f(x) \cdot g(x), s)$$$

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 : StrictMonoOn f s) (hg : StrictMonoOn g s) :
    StrictMonoOn (fun x => f x * g x) s := fun _ ha _ hb ab => mul_lt_mul_of_lt_of_lt (hf ha hb ab) (hg ha hb ab)

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