English
If f and g are monotone-on the set s, then their pointwise product x ↦ f(x) × g(x) is monotone-on the same set s.
Русский
Если f и g монотонны на множестве s, то их поперечное произведение x ↦ f(x) × g(x) монотонно на том же множестве s.
LaTeX
$$$\\bigl(\\operatorname{MonotoneOn} f\\, s\\bigr) \\land \\bigl(\\operatorname{MonotoneOn} g\\, s\\bigr) \\Rightarrow \\operatorname{MonotoneOn}\\bigl(\\lambda x. f(x)\\times g(x)\\bigr)\\, s.$$$
Lean4
theorem _root_.MonotoneOn.set_prod (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ×ˢ g x) s :=
fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)
