mul_monotone' — Mathlib

English

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

Русский

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

LaTeX

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

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

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