English
If hf is strictly monotone on s and hg is monotone on s, then f(x)·g(x) is strictly monotone on s.
Русский
Если hf строго монотонна на s, а hg монотонна на s, то f(x)·g(x) строго монотонно на s.
LaTeX
$$$hf : StrictMonoOn(f,s), hg: MonotoneOn(g,s) \Rightarrow StrictMonoOn(\lambda x. f(x) \cdot g(x), s)$$$
Lean4
/-- The product of a monotone function and a strictly monotone function is strictly monotone. -/
@[to_additive add_strictMono /-- The sum of a monotone function and a strictly monotone function is
strictly monotone. -/
]
theorem mul_strictMono' [MulLeftStrictMono α] [MulRightMono α] {f g : β → α} (hf : MonotoneOn f s)
(hg : StrictMonoOn g s) : StrictMonoOn (fun x => f x * g x) s := fun _ hx _ hy h =>
mul_lt_mul_of_le_of_lt (hf hx hy h.le) (hg hx hy h)
